 6.8. SPECIFYING FUNCOIDS BY FUNCTIONS OR RELATIONS ON ATOMIC FILTERS 113

similarly

X δ

0

I

J

X δ

0

I

X δ

0

J

for suitable

I

and

J

. Let’s continue

δ

0

till a funcoid

f

(by the theorem

595

):

X

[

f

]

Y ⇔ ∀

X

∈ X

, Y

∈ Y

:

X δ

0

Y.

The reverse of (

10

implication is trivial, so

X

a, Y

b

x

atoms

A

X, y

atoms

A

X

:

x δ y

a δ b.

Also

X

a, Y

b

x

atoms

A

X, y

atoms

A

X

:

x δ y

X

a, Y

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

635

.

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

n

h

f

i

x

f

R

o

;

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

a, Y

b

x

atoms

A

X, y

atoms

B

Y

:

x δ y

f

R, X

a, Y

b

x

atoms

A

X, y

atoms

B

Y

:

x

[

f

]

y

f

R, X

a, Y

b

:

X

[

f

]

Y

f

R

:

a

[

f

]

b

a δ b.

So by theorem (

634

),

δ

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

(

B

)

f

R

:

y

u h

f

i

x

6

=

F

(

B

)

y

l

h

atoms

i

h

f

i

x

f

R

y

atoms

l

h

f

i

x

f

R

for every

y

atoms

F

(

A

)

. From this it follows

h

d

R

i

x

=

d

n

h

f

i

x

f

R

o

.