4.3. CATEGORY

REL

65

Proof.

X

[

g

f

]

Z

⇔ ∃

x

X, z

Z

:

x

(

g

f

)

z

x

X, z

Z, β

: (

x f β

β g z

)

β

: (

x

X

:

x f β

∧ ∃

y

Y

:

β g z

)

⇔ ∃

β

: (

X

[

f

]

{

β

} ∧ {

β

}

[

g

]

Z

)

.

Corollary

385

.

X

[

g

f

]

Z

⇔ ∃

y

atoms

T

B

: (

X

[

f

]

y

y

[

g

]

Z

) for

f

Rel

(

A, B

),

g

Rel

(

B, C

) (for sets

A

,

B

,

C

).

Proposition

386

.

f

S

G

=

S

g

G

(

f

g

) and

S

G

f

=

S

g

G

(

g

f

) for every

binary relation

f

and set

G

of binary relations.

Proof.

We will prove only

S

G

f

=

S

g

G

(

g

f

) as the other formula follows

from duality. Really

(

x, z

)

[

G

f

⇔ ∃

y

: ((

x, y

)

f

(

y, z

)

[

G

)

y, g

G

: ((

x, y

)

f

(

y, z

)

g

)

⇔ ∃

g

G

: (

x, z

)

g

f

(

x, z

)

[

g

G

(

g

f

)

.

Corollary

387

.

Every

Rel

-morphism is metacomplete and co-metacomplete.

Proposition

388

.

The following are equivalent for a

Rel

-morphism

f

:

1

.

f

is monovalued.

2

.

f

is metamonovalued.

3

.

f

is weakly metamonovalued.

4

.

h

f

i

a

is either atomic or least whenever

a

atoms

T

Src

f

.

5

.

f

1

(

I

u

J

) =

f

1

I

u

f

1

J

for every

I, J

T

Src

f

.

6

.

f

1

d

S

=

d

Y

S

f

1

Y

for every

S

PT

Src

f

.

Proof.

2

3

Obvious.

1

2

Take

x

atoms

T

Src

f

; then

f x

atoms

T

Dst

f

∪{⊥

T

Dst

f

}

and thus

D

l

G

f

E

x

=

D

l

G

E

h

f

i

x

=

l

g

G

h

g

i

h

f

i

x

=

l

g

G

h

g

f

i

x

=

*

l

g

G

(

g

f

)

+

x

;

so (

d

G

)

f

=

d

g

G

(

g

f

).

3

1

Take

g

=

{

(

a, y

)

}

and

h

=

{

(

b, y

)

}

for arbitrary

a

6

=

b

and arbitrary

y

. We

have

g

h

=

; thus (

g

f

)

(

h

f

) = (

g

h

)

f

=

and thus impossible

x f a

x f b

as otherwise (

x, y

)

(

g

f

)

(

h

f

). Thus

f

is monovalued.