 Proposition 8.13.

h

(

FCD

)

f

iX

=

im

(

f

j

X

)

for every reloid

f

and a lter

X 2

F

(

Src

f

)

.

Proof.

im

(

f

j

X

) =

im

(

FCD

)(

f

j

X

) =

im

(((

FCD

)

f

)

j

X

) =

h

(

FCD

)

f

iX

.

Proposition 8.14.

(

FCD

)

f

=

x

FCD

y

j

x

2

atoms

F

(

Src

f

)

; y

2

atoms

F

(

Src

f

)

; x

RLD

y

/

f

for

every reloid

f

.

Proof.

(

FCD

)

f

=

x

FCD

y

j

x

2

atoms

F

(

Src

f

)

; y

2

atoms

F

(

Dst

f

)

; x

FCD

y

/ (

FCD

)

f

, but

x

FCD

y

/ (

FCD

)

f

,

x

[(

FCD

)

f

]

y

,

x

RLD

y

/

f

, thus follows the theorem.

8.2 Reloids induced by a funcoid

Every funcoid

f

2

FCD

(

A

;

B

)

induces a reloid from

A

to

B

in two ways, intersection of

outward

relations and union of

inward

reloidal products of lters:

(

RLD

)

out

f

=

l

h"

RLD

i

xyGR

f

;

(

RLD

)

in

f

=

G

fA

RLD

B j A 2

F

(

A

)

;

B 2

F

(

B

)

;

FCD

B v

f

g

:

Theorem 8.15.

(

RLD

)

in

f

=

a

RLD

b

j

a

2

atoms

F

(

A

)

; b

2

atoms

F

(

B

)

; a

FCD

b

v

f

.

Proof.

It follows from theorem

7.21

.

Remark 8.16.

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

GR

"

RLD

f

=

GR

"

FCD

f

for every Rel-morphism

f

.

Proof.

X

2

GR

"

RLD

f

,

X

f

,

X

2

GR

"

FCD

f

.

Proposition 8.18.

(

RLD

)

out

"

FCD

f

=

"

RLD

f

for every Rel-morphism

f

.

Proof.

(

RLD

)

out

"

FCD

f

=

d

h"

RLD

i

xyGR

f

=

"

RLD

min xyGR

f

=

"

RLD

f

taking into account the

previous proposition.

Surprisingly, a funcoid is greater inward than outward:

Theorem 8.19.

(

RLD

)

out

f

v

(

RLD

)

in

f

for every funcoid

f

.

Proof.

We need to prove

(

RLD

)

out

f

v

G

fA

RLD

B j A 2

F

(

Src

f

)

;

B 2

F

(

Dst

f

)

;

FCD

B v

f

g

:

Let

K

2

G

fA

RLD

B j A 2

F

(

Src

f

)

;

B 2

F

(

Dst

f

)

;

FCD

B v

f

g

:

Then

K

2 "

RLD

(

Src

f

;

Dst

f

)

[

f

X

A

Y

B

j A 2

F

(

Src

f

)

;

B 2

F

(

Dst

f

)

;

FCD

B v

f

g

= (

RLD

)

out

"

FCD

[

f

X

A

Y

B

j A 2

F

(

Src

f

)

;

B 2

F

(

Dst

f

)

;

FCD

B v

f

g

= (

RLD

)

out

G

f"

FCD

(

X

A

Y

B

)

j A 2

F

(

Src

f

)

;

B 2

F

(

Dst

f

)

;

FCD

B v

f

g

w

(

RLD

)

out

G

atoms

f

= (

RLD

)

out

f

where

X

A

2 A

,

Y

B

2 B

. So

K

2

(

RLD

)

out

f

.

Theorem 8.20.

(

FCD

)(

RLD

)

in

f

=

f

for every funcoid

f

.

134

Relationships between funcoids and reloids