 4.4. PRODUCT OF TYPED SETS

66

4

6

Let

a

atoms

T

Src

f

,

h

f

i

a

=

b

.

Then because

b

atoms

T

Dst

f

∪{⊥

T

Dst

f

}

l

S

u

b

6

=

⊥ ⇔ ∀

Y

S

:

Y

u

b

6

=

;

a

[

f

]

l

S

⇔ ∀

Y

S

:

a

[

f

]

Y

;

l

S

f

1

a

⇔ ∀

Y

S

:

Y

f

1

a

;

a

6

f

1

l

S

⇔ ∀

Y

S

:

a

6

f

1

Y

;

a

6

f

1

l

S

a

6

l

Y

S

f

1

Y

;

f

1

l

S

=

l

X

S

f

1

X.

6

5

Obvious.

5

1

.

f

1

a

u

f

1

b

=

f

1

(

a

u

b

) =

f

1

=

for every two distinct

atoms

a

=

{

α

}

, b

=

{

β

} ∈

T

Dst

f

. From this

α

(

f

f

1

)

β

⇔ ∃

y

Dst

f

: (

α f

1

y

y f β

)

y

Dst

f

: (

y

f

1

a

y

f

1

b

)

is impossible. Thus

f

f

1

v

1

Rel

Dst

f

.

¬

4

⇒ ¬

1

Suppose

h

f

i

a /

atoms

T

Dst

f

∪{⊥

T

Dst

f

}

for some

a

atoms

T

Src

f

.

Then there exist distinct points

p

,

q

such that

p, q

∈ h

f

i

a

. Thus

p

(

f

f

1

)

q

and so

f

f

1

6v

1

Rel

Dst

f

.

4.4. Product of typed sets

Definition

386

.

Product of typed sets is defined by the formula

(

P

U, A

)

×

(

P

W, B

) = (

U, W, A

×

B

)

.

Proposition

387

.

Product of typed sets is a

Rel

-morphism.

Proof.

We need to prove

A

×

B

U

×

W

, but this is obvious.

Obvious

388

.

Atoms of

Rel

(

A, B

) are exactly products

a

×

b

where

a

and

b

are atoms correspondingly of

T

A

and

T

B

.

Rel

(

A, B

) is an atomistic poset.

Proposition

389

.

f

6

A

×

B

A

[

f

]

B

for every

Rel

-morphism

f

and

A

T

Src

f

,

B

T

Dst

f

.

Proof.

A

[

f

]

B

⇔ ∃

x

atoms

A, y

atoms

B

:

x

[

f

]

y

x

atoms

T

Src

f

, y

atoms

T

Dst

f

: (

x

×

y

v

f

x

×

y

v

A

×

B

)

f

6

A

×

B.

Definition

390

.

Image

and

domain

of a

Rel

-morphism

f

are typed sets de-

fined by the formulas

dom(

U, W, f

) = (

P

U,

dom

f

) and im(

U, W, f

) = (

P

W,

im

f

)

.

Obvious

391

.

Image and domain of a

Rel

-morphism are really typed sets.

Definition

392

.

Restriction

of a

Rel

-morphism to a typed set is defined by

the formula (

U, W, f

)

|

(

P

U,X

)

= (

U, W, f

|

X

).