 Proof

Let

a

be an atomic filter object on Src

f

.

h

(

FCD

)

f

i

a

=

FCD

(Src

f

;Dst

f

)

F

a

|

F

up

f

by the definition of

(

FCD

).

FCD

(Src

f

;Dst

f

)

up

f

a

=

FCD

(Src

f

;Dst

f

)

F

a

|

F

up

f

by

the theorem 17.

So

h

(

FCD

)

f

i

a

=

FCD

(Src

f

;Dst

f

)

up

f

a

for every

a

.

Lemma 4

For every two filter bases

S

and

T

of binary relations on

U

×

V

for

some small sets

U

,

V

and every set

A

U

\ D

RLD

(

U

;

V

)

E

S

=

\ D

RLD

(

U

;

V

)

E

T

V

h

F

i

A

|

F

S

=

V

h

G

i

A

|

G

T

.

Proof

Let

RLD

(

U

;

V

)

S

=

RLD

(

U

;

V

)

T

.

First let prove that

{h

F

i

A

|

F

S

}

is a filter base. Let

X, Y

∈ {h

F

i

A

|

F

S

}

.

Then

X

=

h

F

X

i

A

and

Y

=

h

F

Y

i

A

for some

F

X

, F

Y

S

.

Because

S

is a filter base, we have

S

F

Z

F

X

F

Y

. So

h

F

Z

i

A

X

Y

and

h

F

Z

i

A

∈ {h

F

i

A

|

F

S

}

. So

{h

F

i

A

|

F

S

}

is a filter base.

Suppose

X

up

V

h

F

i

A

|

F

S

. Then exists

X

∈ {h

F

i

A

|

F

S

}

where

X

X

because

{h

F

i

A

|

F

S

}

is a filter base. That is

X

=

h

F

i

A

for some

F

S

. There exists

G

T

such that

G

F

because

T

is a filter

base. Let

Y

=

h

G

i

A

. We have

Y

X

X

;

Y

∈ {h

G

i

A

|

G

T

}

;

Y

up

V

h

G

i

A

|

G

T

;

X

up

V

h

G

i

A

|

G

T

. The re-

verse is symmetric.

Lemma 5

{

G

F

|

F

up

f, G

up

g

}

is a filter base for every reloids

f

and

g

.

Proof

Let denote

D

=

{

G

F

|

F

up

f, G

up

g

}

. Let

A

D

B

D

.

Then

A

=

G

A

F

A

B

=

G

B

F

B

for some

F

A

, F

B

up

f

and

G

A

, G

B

up

g

. So

A

B

(

G

A

G

B

)

(

F

A

F

B

)

D

because

F

A

F

B

up

f

and

G

A

G

B

up

g

.

Theorem 63

(

FCD

)(

g

f

) = ((

FCD

)

g

)

((

FCD

)

f

)

for every composable reloids

f

and

g

.

Proof

h

(

FCD

)(

g

f

)

i

X

=

Dst

g

h

H

i

X

|

H

up(

g

f

)

=

\ n

Dst

g

h

H

i

X

|

H

up

\ n

RLD

(Src

f

;Dst

g

)

(

G

F

)

|

F

up

f, G

up

g

oo

.

Obviously

\ n

RLD

(Src

f

;Dst

g

)

(

G

F

)

|

F

up

f, G

up

g

o

=

\ D

RLD

(Src

f

;Dst

g

)

E

up

\ n

RLD

(Src

f

;Dst

g

)

(

G

F

)

|

F

up

f, G

up

g

o

;

53