4.3. CATEGORY

REL

64

4

From two previous formulas.

5

.

X

[

f

]

Y

⇔ ∃

α

X, β

Y

:

α f β

⇔ ∃

α

X, β

Y

:

{

α

}

[

f

]

{

β

}

.

6

Obvious.

Corollary

377

.

For a

Rel

-morphism

f

we have:

1

.

h

f

i

d

S

=

d

h

f

i

S

for

S

PT

Src

f

;

2

.

d

S

[

f

]

Y

⇔ ∃

X

S

:

X

[

f

]

Y

for

S

PT

Src

f

;

3

.

X

[

f

]

d

T

⇔ ∃

Y

T

:

X

[

f

]

Y

for

T

PT

Dst

f

;

4

.

d

S

[

f

]

d

T

⇔ ∃

X

S, Y

T

:

X

[

f

]

Y

for

S

PT

Src

f

,

T

PT

Dst

f

;

5

.

X

[

f

]

Y

⇔ ∃

x

atoms

X, y

atoms

Y

:

x

[

f

]

y

for

X

T

Src

f

,

Y

T

Dst

f

;

6

.

h

f

i

X

=

d

h

f

i

atoms

X

for

X

T

Src

f

.

Corollary

378

.

A

Rel

-morphism

f

can be restored knowing either

h

f

i

x

for

atoms

x

T

Src

f

or

x

[

f

]

y

for atoms

x

T

Src

f

,

y

T

Dst

f

.

Proposition

379

.

Let

A

,

B

be sets,

R

be a set of binary relations.

1

.

h

S

R

i

X

=

S

f

R

h

f

i

X

for every set

X

;

2

.

h

T

R

i

{

α

}

=

T

f

R

h

f

i

{

α

}

for every

α

, if

R

is nonempty;

3

.

X

[

S

R

]

Y

⇔ ∃

f

R

:

X

[

f

]

Y

for every sets

X

,

Y

;

4

.

α

(

T

R

)

β

⇔ ∀

f

R

:

α f β

for every

α

and

β

, if

R

is nonempty.

Proof.

1

.

y

D[

R

E

X

⇔ ∃

x

X

:

x

[

R

y

⇔ ∃

x

X, f

R

:

x f y

f

R

:

y

∈ h

f

i

X

y

[

f

R

h

f

i

X.

2

.

y

D\

R

E

{

α

} ⇔ ∀

f

R

:

α f y

⇔ ∀

f

R

:

y

∈ h

f

i

{

α

} ⇔

y

\

f

R

h

f

i

{

α

}

.

3

.

X

h[

R

i

Y

⇔ ∃

x

X, y

Y

:

x

[

R

y

x

X, y

Y, f

R

:

x f y

⇔ ∃

f

R

:

X

[

f

]

Y.

4

Obvious.

Corollary

380

.

Let

A

,

B

be sets,

R

P

Rel

(

A, B

).

1

.

h

d

R

i

X

=

d

f

R

h

f

i

X

for

X

T

A

;

2

.

h

d

R

i

x

=

d

f

R

h

f

i

x

for atomic

x

T

A

;

3

.

X

[

d

R

]

Y

⇔ ∃

f

R

:

X

[

f

]

Y

for

X

T

A

,

Y

T

B

;

4

.

x

[

d

R

]

y

⇔ ∀

f

R

:

x

[

f

]

y

for every atomic

x

T

A

,

y

T

B

.

Proposition

381

.

X

[

g

f

]

Z

⇔ ∃

β

: (

X

[

f

]

{

β

} ∧ {

β

}

[

g

]

Z

) for every

binary relation

f

and sets

X

and

Y

.