background image

9.3. LEMMAS FOR THE MAIN RESULT

158

Let

X

dom

d

n

RLD

(Src

f

×

Dst

g

)

(

G

F

)

F

GR

f,G

GR

g

o

. Then there exist

Y

such that

X

×

Y

l

RLD

(Src

f

×

Dst

g

)

(

G

F

)

F

GR

f, G

GR

g

.

So because it is a generalized filter base

X

×

Y

G

F

for some

F

GR

f

,

G

GR

g

. Thus

X

dom(

G

F

).

X

GR(

g

f

).

We can define

g

f

for reloids

f

,

g

:

g

f

=

G

F

F

GR

f, G

GR

g

.

Then

g

f

=

l

D

RLD

(Src

f

;Dst

g

)

E

h

dom

i

(

g

f

) = dom

D

RLD

(Src

f

×

Dst

g

;

f

)

E

(

g

f

)

9.3. Lemmas for the main result

Lemma

853

.

(

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

854

.

Let

F

=

RLD

(Src

F

;Dst

F

)

f

be a principal reloid,

T

is a set of

reloids from Dst

F

to a set

V

.

l

RLD

(Src

f

×

V

;

f

)

(

G

f

)

G

GR

F

T

=

G

(

d

RLD

(Src

f

×

V

;

f

)

(

G

F

)

G

T

)

.

Proof.

d

RLD

(Src

f

×

V

;

f

)

(

G

f

)

G

GR

F

T

w

F

d

h

RLD

(Src

f

×

V

;

f

)

i

(

G

F

)

G

T

is obvious.

Let

K

F

d

h

RLD

(Src

f

×

V

;

f

)

i

(

G

F

)

G

T

. Then for each

G

T

K

l

D

RLD

(Src

f

×

V

;

f

)

E

(

G

F

);

K

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

GR

F

T

.

K

n

0

f

)

∩···∩

n

f

)

n

N

o

. So

K

0

0

f

)

∩ · · · ∩

0

n

f

)

n

N

,

Γ

0

i

GR

F

T

=

0

0

∩ · · · ∩

Γ

0

n

)

f

n

N

,

Γ

0

i

GR

F

T

=

l

D

RLD

(Src

f

×

V

;

f

)

E

G

f

G

GR

F

T

.