8.2. RELOIDS INDUCED BY A FUNCOID

151

8.2. Reloids induced by a funcoid

Every funcoid

f

FCD

(

A

;

B

) induces a reloid from

A

to

B

in two ways,

intersection of

outward

relations and union of

inward

reloidal products of filters:

(

RLD

)

out

f

=

l

RLD

xyGR

f

;

(

RLD

)

in

f

=

G

A ×

RLD

B

A ∈

F

(

A

)

,

B ∈

F

(

B

)

,

A ×

FCD

B v

f

.

Theorem

813

.

(

RLD

)

in

f

=

F

n

a

×

RLD

b

a

atoms

F

(

A

)

,b

atoms

F

(

B

)

,a

×

FCD

b

v

f

o

.

Proof.

It follows from theorem

751

.

Remark

814

.

It seems that (

RLD

)

in

has smoother properties and is more

important than (

RLD

)

out

. (However see also the exercise below for (

RLD

)

in

not

preserving identities.)

Proposition

815

.

GR

RLD

f

= GR

FCD

f

for every

Rel

-morphism

f

.

Proof.

X

GR

RLD

f

X

f

X

GR

FCD

f

.

Proposition

816

.

(

RLD

)

out

FCD

f

=

RLD

f

for every

Rel

-morphism

f

.

Proof.

(

RLD

)

out

FCD

f

=

d

RLD

xyGR

f

=

RLD

min xyGR

f

=

RLD

f

taking into account the previous proposition.

Surprisingly, a funcoid is greater inward than outward:

Theorem

817

.

(

RLD

)

out

f

v

(

RLD

)

in

f

for every funcoid

f

.

Proof.

We need to prove

(

RLD

)

out

f

v

G

A ×

RLD

B

A ∈

F

(

A

)

,

B ∈

F

(

B

)

,

A ×

FCD

B v

f

.

Let

K

G

A ×

RLD

B

A ∈

F

(

A

)

,

B ∈

F

(

B

)

,

A ×

FCD

B v

f

.

Then

K

∈↑

RLD

(Src

f

;Dst

f

)

[

X

A

×

Y

B

A ∈

F

(

A

)

,

B ∈

F

(

B

)

,

A ×

FCD

B v

f

= (

RLD

)

out

FCD

[

X

A

×

Y

B

A ∈

F

(

A

)

,

B ∈

F

(

B

)

,

A ×

FCD

B v

f

= (

RLD

)

out

G

FCD

(

X

A

×

Y

B

)

A ∈

F

(

A

)

,

B ∈

F

(

B

)

,

A ×

FCD

B v

f

w

(

RLD

)

out

G

atoms

f

= (

RLD

)

out

f

where

X

A

∈ A

,

X

B

∈ B

.

K

(

RLD

)

out

f

.

Theorem

818

.

(

FCD

)(

RLD

)

in

f

=

f

for every funcoid

f

.