 Proof.

Let

f

be bijective. Then

f

f

y

v

1

Dst

f

,

f

y

f

w

1

Src

f

,

f

y

f

v

1

Src

f

,

f

f

y

w

1

Dst

f

. Thus

f

f

y

= 1

Dst

f

and

f

y

f

= 1

Src

f

that is

f

y

is an inverse of

f

.

[TODO: Below require that Mor-sets are complete lattices.]

Denition 3.61.

A morphism

f

of a partially ordered category is

metamonovalued

when

(

d

G

)

f

=

d

g

2

G

(

g

f

)

whenever

G

is a set of morphisms with a suitable domain and image.

Denition 3.62.

A morphism

f

of a partially ordered category is

metainjective

when

f

(

d

G

) =

d

g

2

G

(

f

g

)

whenever

G

is a set of morphisms with a suitable domain and image.

Obvious 3.63.

Metamonovaluedness and metainjectivity are dual to each other.

Denition 3.64.

A morphism

f

of a partially ordered category is

metacomplete

when

f

(

F

G

) =

d

g

2

G

(

f

g

)

whenever

G

is a set of morphisms with a suitable domain and image.

Denition 3.65.

A morphism

f

of a partially ordered category is

co-metacomplete

when

(

F

G

)

f

=

d

g

2

G

(

g

f

)

whenever

G

is a set of morphisms with a suitable domain and image.

3.6 Partitioning

Denition 3.66.

Let

A

be a complete lattice.

Torning

of an element

a

2

A

is a set

S

2

P

A

n f

0

g

such that

G

S

=

a

and

8

x; y

2

S

: (

x

=

/

y

)

x

y

)

:

Denition 3.67.

Let

A

be a complete lattice.

Weak partition

of an element

a

2

A

is a set

S

2

P

A

n f

0

g

such that

G

S

=

a

and

8

x

2

S

:

x

G

(

S

n f

x

g

)

:

Denition 3.68.

Let

A

be a complete lattice.

Strong partition

of an element

a

2

A

is a set

S

2

P

A

n f

0

g

such that

G

S

=

a

and

8

A; B

2

P

S

:

¡

A

B

)

G

A

G

B

:

Obvious 3.69.

1. Every strong partition is a weak partition.
2. Every weak partition is a torning.

3.7 A proposition about binary relations

Proposition 3.70.

Let

f

,

g

,

h

be binary relations. Then

g

f

/

h

,

g

/

h

f

¡

1

.

Proof.

g

f

/

h

,

9

a; c

:

a

((

g

f

)

\

h

)

c

,

9

a; c

: (

a

(

g

f

)

c

^

a h c

)

,

9

a; b; c

: (

a f b

^

b g c

^

a h c

)

,

9

b; c

: (

b g c

^

b

(

h

f

¡

1

)

c

)

,

9

b; c

: (

b

(

g

\

(

h

f

¡

1

))

c

)

,

g

/

h

f

¡

1

:

42

More on order theory