 7.9. SPECIFYING FUNCOIDS BY FUNCTIONS OR RELATIONS ON ATOMIC FILTERS 162

The reverse of (

12

implication is trivial, so

X

up

a, Y

up

b

x

atoms

X, y

atoms

Y

:

x δ y

a δ b.

Also

X

up

a, Y

up

b

x

atoms

X, y

atoms

Y

:

x δ y

X

up

a, Y

up

b

:

X δ

0

Y

a

[

f

]

b.

So

a δ b

a

[

f

]

b

, that is [

f

] is a continuation of

δ

.

One of uses of the previous theorem is the proof of the following theorem:

Theorem

875

.

If

A

and

B

are sets,

R

P

FCD

(

A, B

),

x

atoms

F

(

A

)

,

y

atoms

F

(

B

)

, then

1

.

h

d

R

i

x

=

d

f

R

h

f

i

x

;

2

.

x

[

d

R

]

y

⇔ ∀

f

R

:

x

[

f

]

y

.

Proof.

2

Let denote

x δ y

⇔ ∀

f

R

:

x

[

f

]

y

. For every

a

atoms

F

(

A

)

,

b

atoms

F

(

B

)

X

up

a, Y

up

b

x

atoms

X, y

atoms

Y

:

x δ y

f

R, X

up

a, Y

up

b

x

atoms

X, y

atoms

Y

:

x

[

f

]

y

f

R, X

up

a, Y

up

b

:

X

[

f

]

Y

f

R

:

a

[

f

]

b

a δ b.

So by theorem

874

,

δ

can be continued till [

p

] for some funcoid

p

FCD

(

A, B

).

For every funcoid

q

FCD

(

A, B

) such that

f

R

:

q

v

f

we have

x

[

q

]

y

⇒ ∀

f

R

:

x

[

f

]

y

x δ y

x

[

p

]

y,

so

q

v

p

. Consequently

p

=

d

R

.

From this

x

[

d

R

]

y

⇔ ∀

f

R

:

x

[

f

]

y

.

1

From the former

y

atoms

D

l

R

E

x

y

u

D

l

R

E

x

6

=

⊥ ⇔

f

R

:

y

u h

f

i

x

6

=

⊥ ⇔

y

l

h

atoms

i

h

f

i

x

f

R

y

atoms

l

f

R

h

f

i

x

for every

y

atoms

F

(

A

)

. From this it follows

h

d

R

i

x

=

d

f

R

h

f

i

x

.

Theorem

876

.

g

f

=

d

FCD

n

G

F

F

up

f.G

up

g

o

for every composable funcoids

f

and

g

.