 8.7. COMPLETE RELOIDS AND COMPLETION OF RELOIDS

195

Proof.

Compl

l

R

=

l

(

d

R

)

|

A

{

α

}

α

A

= (theorem

610

)

l

d

n

f

|

↑{

α

}

α

A

o

f

R

=

l

h

Compl

i

R.

Lemma

1056

.

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

=

l

F

(

α

)

×

RLD

Dst

f

{

α

}

α

Dst

f

.

So

Compl

f

=

l

d

n

F

(

α

)

×

RLD

Dst

f

{

α

}

α

Dst

f

o

|

↑{

β

}

β

Src

f

=

l

d

n

F

(

α

)

×

RLD

Dst

f

{

α

}

α

Dst

f

o

u

(

Src

f

{

β

} ×

RLD

>

F

(Dst

f

)

)

β

Src

f

= (*)

l

d

n

(

F

(

α

)

×

RLD

Dst

f

{

α

}

)

u

(

Src

f

{

β

RLD

>

F

(Dst

f

)

)

α

Dst

f

o

β

Src

f

=

l

d

n

Src

f

{

β

RLD

Dst

f

{

α

}

α

Dst

f

o

β

Src

f,

Src

f

{

β

} v

F

(

α

)

* theorem

610

.

Thus Compl

f

is principal.

Theorem

1057

.

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

.

Conjecture

1058

.

If

f

is a complete reloid, then it is metacomplete.

Conjecture

1059

.

If

f

is a metacomplete reloid, then it is complete.

Conjecture

1060

.

Compl

f

=

f

\

(Ω

Src

f

×

RLD

>

F

(Dst

f

)

) for every reloid

f

.

By analogy with similar properties of funcoids described above: