background image

10.3. LEMMAS FOR THE MAIN RESULT

216

Proof.

F

(Src

f

×

Dst

g

)

dom(

G

F

)

w

dom

d

F

(Src

f

×

Dst

g

)

n

G

F

F

GR

f,G

GR

g

o

.

Thus

g

f

w

dom

F

(Src

f

×

Dst

g

)

l

G

F

F

GR

f, G

GR

g

.

Let

X

up dom

d

F

(Src

f

×

Dst

g

)

n

G

F

F

up

f,G

up

g

o

. Then there exist

Y

such that

X

×

Y

up

F

(Src

f

×

Dst

g

)

l

G

F

F

up

f, G

up

g

.

So because it is a generalized filter base

X

×

Y

G

F

for some

F

up

f

,

G

up

g

.

Thus

X

up dom(

G

F

).

X

up(

g

f

).

We can define

g

f

for reloids

f

,

g

:

g

f

=

G

F

F

GR

f, G

GR

g

.

Then

g

f

=

F

(Src

f

×

Dst

g

)

l

h

dom

i

(

g

f

) = dom

D

RLD

(Src

f

×

Dst

g,

f

)

E

(

g

f

)

.

10.3. Lemmas for the main result

Lemma

1158

.

(

g

f

)

(

h

f

) = (

g

h

)

f

for binary relations

f

,

g

,

h

.

Proof.

(

g

h

)

f

= Θ

0

f

Θ

1

(

g

h

) = Θ

0

f

1

g

Θ

1

h

) =

0

f

Θ

1

g

)

0

f

Θ

1

h

) = (

g

f

)

(

h

f

)

.

Lemma

1159

.

Let

F

=

RLD

f

be a principal reloid (for a

Rel

-morphism

f

),

T

be a set of reloids from Dst

F

to a set

V

.

RLD

(Src

f

×

V,

f

)

l

G

up

d

T

(

G

f

) =

l

G

T

RLD

(Src

f

×

V,

f

)

l

(

G

F

)

.

Proof.

d

RLD

(Src

f

×

V,

f

)

G

up

d

T

(

G

f

)

w

d

G

T

d

RLD

(Src

f

×

V,

f

)

(

G

F

) is obvious.

Let

K

up

d

G

T

d

RLD

(Src

f

×

V,

f

)

(

G

F

). Then for each

G

T

K

up

RLD

(Src

f

×

V,

f

)

l

(

G

F

);

K

up

d

RLD

(Src

f

×

V,

f

)

n

Γ

f

Γ

G

o

. Then

K

n

Γ

f

Γ

G

o

by properties of generalized

filter bases.

K

n

0

∩···∩

Γ

n

)

f

n

N

,

Γ

i

G

o

=

n

0

f

)

∩···∩

n

f

)

n

N

,

Γ

i

G

o

.

G

T

:

K

G,

0

f

)

∩ · · · ∩

G,n

f

) for some

n

N

, Γ

G,i

G

.

K

n

0

f

)

∩···∩

n

f

)

n

N

,

Γ

i

G

o

where Γ

i

=

S

g

G

Γ

g,i

up

d

T

.