 We can dene

g

f

for reloids

f

,

g

:

g

f

=

f

G

F

j

F

2

GR

f ; G

2

GR

g

g

:

Then

g

f

=

l

"

RLD

(

Src

f

;

Dst

g

)

h

dom

i

(

g

f

) =

dom

l

"

RLD

(

Src

f

Dst

g

;

f

)

(

g

f

)

:

9.3 Lemmas for the main result

Lemma 9.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 9.6.

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

)

j

G

2

GR

G

T

=

l

"

RLD

(

Src

f

V

;

f

)

(

G

F

)

j

G

2

T

:

Proof.

d

"

RLD

(

Src

f

V

;

f

)

(

G

f

)

j

G

2

GR

F

T

w

d

"

RLD

(

Src

f

V

;

f

)

(

G

F

)

j

G

2

T

is

obvious.

Let

K

2

d

"

RLD

(

Src

f

V

;

f

)

(

G

F

)

j

G

2

T

. Then for each

G

2

T

K

2

l

"

RLD

(

Src

f

V

;

f

)

(

G

F

);

K

2

d

"

RLD

(

Src

f

V

;

f

)

f

¡

f

j

¡

2

G

g

.

Then

K

2 f

¡

f

j

¡

2

GR

G

g

by properties of generalized lter bases.

K

2 f

0

\

:::

\

¡

n

)

f

j

n

2

N

;

¡

i

2

G

g

=

f

0

f

)

\

:::

\

n

f

)

j

n

2

N

;

¡

i

2

G

g

.

8

G

2

T

:

K

G;

0

f

)

\

:::

\

G;n

f

)

for some

n

2

N

;

¡

G;i

2

G

.

K

0

f

)

\

:::

\

n

f

)

where

¡

i

=

S

g

2

G

¡

g;i

2

GR

F

T

.

K

2 f

0

f

)

\

:::

\

n

f

)

j

n

2

N

g

.

So

K

2 f

0

0

f

)

\

:::

\

n

0

f

)

j

n

2

N

;

¡

i

0

2

GR

F

T

g

=

f

0

0

\

:::

\

¡

n

0

)

f

j

n

2

N

;

¡

i

0

2

GR

F

T

g

=

d

"

RLD

(

Src

f

V

;

f

)

f

G

f

j

G

2

GR

F

T

g

.

9.4 Proof of the main result

Theorem 9.7.

(

F

T

)

F

=

F

f

G

F

j

G

2

T

g

for every principal reloid

F

=

"

RLD

(

Src

f

;

Dst

g

)

f

and

a set

T

of reloids from Dst

F

to some set

V

. (In other words principal reloids are co-metacomplete

and thus also metacomplete by duality.)

Proof.

¡G

T

F

=

l

"

RLD

(

Src

f

;

V

)

h

dom

i

¡¡G

T

F

=

dom

l

"

RLD

(

Src

f

V

;

f

)

¡¡G

T

F

=

dom

l

"

RLD

(

Src

f

V

;

f

)

G

f

j

G

2

GR

G

T

;

G

f

G

F

j

G

2

T

g

=

l

"

RLD

(

Src

f

;

V

)

h

dom

i

(

G

F

)

j

G

2

T

=

dom

l

"

RLD

(

Src

f

V

;

f

)

(

G

F

)

j

G

2

T

=

dom

l

"

RLD

(

Src

f

V

;

f

)

(

G

F

)

j

G

2

T

:

It's enough to prove

l

"

RLD

(

Src

f

V

;

f

)

(

G

f

)

j

G

2

GR

G

T

=

l

"

RLD

(

Src

f

V

;

f

)

(

G

F

)

j

G

2

T

140

On distributivity of composition with a principal reloid