7.7. COMPLETE RELOIDS AND COMPLETION OF RELOIDS

144

Proof.

Compl

G

R

=

G

(

F

R

)

|

A

{

α

}

α

A

= (proposition

461

)

G

F

n

f

|

A

{

α

}

α

A

o

f

R

=

G

h

Compl

i

R.

Lemma

791

.

Completion of a co-complete reloid is principal.

Proof.

Let

f

be a co-complete reloid. Then there is a function

F

: Dst

f

F

(Src

f

) such that

f

=

G

F

(

α

)

×

RLD

Dst

f

{

α

}

α

Dst

f

.

So

Compl

f

=

G

F

n

F

(

α

)

×

RLD

Dst

f

{

α

}

α

Dst

f

o

|

Src

f

{

β

}

β

Src

f

=

G

F

n

F

(

α

)

×

RLD

Dst

f

{

α

}

α

Dst

f

o

u

(

Src

f

{

β

} ×

RLD

>

F

(Dst

f

)

)

β

Src

f

= (*)

G

F

n

(

F

(

α

)

×

RLD

Dst

f

{

α

}

)

u

(

Src

f

{

β

RLD

>

F

(Dst

f

)

)

α

Dst

f

o

β

Src

f

=

G

F

n

Src

f

{

β

RLD

Dst

f

{

α

}

α

Dst

f

o

β

Src

f,

Src

f

{

β

]

v

F

(

α

)

* proposition

461

.

Thus Compl

f

is principal.

Theorem

792

.

Compl CoCompl

f

= CoCompl Compl

f

= Cor

f

for every

reloid

f

.

Proof.

We will prove only Compl CoCompl

f

= Cor

f

. The rest follows from

symmetry.

From the lemma Compl CoCompl

f

is principal.

It is obvious

Compl CoCompl

f

v

f

. So to finish the proof we need to show only that

for every principal reloid

F

v

f

we have

F

v

Compl CoCompl

f

.

Really, obviously

F

v

CoCompl

f

and thus

F

= Compl

F

v

Compl CoCompl

f

.

Question

793

.

Is

ComplRLD

(

A

;

B

) a distributive lattice? Is

ComplRLD

(

A

;

B

)

a co-brouwerian lattice?

FiXme

: Solved.

Conjecture

794

.

If

f

is a complete reloid, then it is metacomplete.

Conjecture

795

.

If

f

is a metacomplete reloid, then it is complete.