background image

Let

X

dom

d

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

F

GR

f , G

GR

g

 

. Then there exist

Y

such that

X

×

Y

d

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

RLD

(

Src

f

;

Dst

g

)

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

RLD

(

Src

f

;

Dst

g

)

h

dom

i

(

g

f

) =

dom

l

RLD

(

Src

f

×

Dst

g

;

)

(

g

f

)

.

2 Lemmas for the main result

Let

F

=

RLD

(

Src

F

;

Dst

F

)

f

is a principal reloid.

Lemma 5.

(

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 6.

d

RLD

(

Src

f

×

Dst

g

;

)

(

G

f

)

|

G

F

T

 

=

d

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

G

T

 

.

Proof.

d

RLD

(

Src

f

×

Dst

g

;

)

(

G

f

)

|

G

GR

F

T

 

d

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

G

T

 

is obvious.

Let

K

d

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

G

T

 

. Then for each

G

T

K

l

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

);

K

d

RLD

(

Src

f

×

Dst

g

;

)

{

Γ

f

|

Γ

GR

G

}

.

K

∈ {

0

f

)

n

f

)

|

n

N

,

Γ

i

GR

G

}

.

G

T

:

K

G,

0

f

)

G,n

f

)

for some

n

N

,

Γ

G,i

G

.

Let

G

T

T

.

K

0

f

)

n

f

)

where

Γ

i

=

S

g

G

Γ

g,i

GR

F

T

.

K

∈ {

0

f

)

n

f

)

|

n

N

}

.

So

K

∈ {

0

f

)

n

f

)

|

n

N

,

Γ

i

GR

F

T

}

=

d

RLD

(

Src

f

×

Dst

g

;

)

{

G

f

|

G

GR

F

T

}

.

3 Proof of the main result

Theorem 7.

(

F

T

)

F

=

F

{

G

F

|

G

T

}

for every principal reloid

F

=

RLD

(

Src

f

;

Dst

g

)

f

.

Proof.

G

T

F

=

l

RLD

(

Src

f

;

Dst

g

)

h

dom

i

G

T

F

=

dom

l

RLD

(

Src

f

×

Dst

g

;

)

G

T

F

=

dom

l

RLD

(

Src

f

×

Dst

g

;

)

 

G

f

|

G

GR

G

T

 

G

{

G

F

|

G

T

}

=

l

RLD

(

Src

f

;

Dst

g

)

h

dom

i

(

G

F

)

|

G

T

 

=

dom

l

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

G

T

 

=

dom

l

RLD

(

Src

f

×

Dst

g

;

)

(

G

F

)

|

G

T

 

.

2

Section 3