background image

The above formula is equivalent to:

F

up

f

:

X

h

FCD

(Src

f

;Dst

f

)

F

i

Y

Y ∩

\ nD

FCD

(Src

f

;Dst

f

)

F

E

X

|

F

up

f

o

6

= 0

F

(Dst

f

)

X ∩

\ nD

FCD

(Src

f

;Dst

f

)

F

1

E

Y

|

F

up

f

o

6

= 0

F

(Src

f

)

.

We have

Y∩

FCD

(Src

f

;Dst

f

)

F

X

|

F

up

f

 

=

Y ∩

FCD

(Src

f

;Dst

f

)

F

X

|

F

up

f

 

.

Let’s denote

W

=

Y ∩

FCD

(Src

f

;Dst

f

)

F

X

|

F

up

f

 

.

F

up

f

:

X

FCD

(Src

f

;Dst

f

)

F

Y ⇔ ∀

F

up

f

:

Y∩

FCD

(Src

f

;Dst

f

)

F

X 6

=

0

F

(Dst

f

)

0

F

(Dst

f

)

6∈

W

.

We need to prove only that 0

F

(Dst

f

)

6∈

W

T

W

6

= 0

F

(Dst

f

)

. (The rest

follows from symmetry.)

This follows from the fact that

W

is a generalized filter base.

Let’s prove that

W

is a generalized filter base. For this it’s enough to prove

that

V

=

FCD

(Src

f

;Dst

f

)

F

X

|

F

up

f

 

is a generalized filter base. Let

A

,

B ∈

V

that is

A

=

FCD

(Src

f

;Dst

f

)

P

X

,

B

=

FCD

(Src

f

;Dst

f

)

Q

X

where

P, Q

up

f

. Then for

C

=

FCD

(Src

f

;Dst

f

)

(

P

Q

)

X

is true both

C ∈

V

and

C ⊆ A

,

B

. So

V

is a generalized filter base and thus

W

is a generalized filter

base.

Proposition 31

(

FCD

)

RLD

(

A

;

B

)

f

=

FCD

(

A

;

B

)

f

for every small sets

A

,

B

and binary relation

f

A

×

B

.

Proof

X

(

FCD

)

RLD

(

A

;

B

)

f

Y ⇔ ∀

F

up

RLD

(

A

;

B

)

f

:

X

FCD

(

A

;

B

)

F

Y ⇔ X

FCD

(

A

;

B

)

f

Y

(for every

X ∈

F

(

A

),

Y ∈

F

(

B

)).

Theorem 61

X

[(

FCD

)

f

]

Y ⇔

(

X ×

RLD

Y

)

6≍

f

for every

f

RLD

and

X ∈

F

(Src

f

)

,

Y ∈

F

(Dst

f

)

.

Proof

(

X ×

RLD

Y

)

6≍

f

⇔ ∀

F

up

f, P

up(

X ×

RLD

Y

) :

P

6≍

F

⇔ ∀

F

up

f, X

up

X

, Y

up

Y

: (

X

×

Y

)

6≍

F

⇔ ∀

F

up

f, X

up

X

, Y

up

Y

:

Src

f

X

h

FCD

(Src

f

;Dst

f

)

F

i

Dst

f

Y

⇔ ∀

F

up

f

:

X

h

FCD

(Src

f

;Dst

f

)

F

i

Y

⇔ X

[(

FCD

)

f

]

Y

.

Theorem 62

(

FCD

)

f

=

FCD

(Src

f

;Dst

f

)

up

f

for every reloid

f

.

52