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

Proof.

Existence of no more than one such funcoids and formulas (

9

and

(

11

follow from the previous theorem.

1

Consider the function

α

0

F

(

B

)

P

A

defined by the formula (for every

X

P

A

)

α

0

X

=

G

h

α

i

atoms

A

X.

Obviously

α

0

=

F

(

B

)

. For every

I, J

P

A

α

0

(

I

J

) =

G

h

α

i

atoms

A

(

I

J

) =

G

h

α

i

(atoms

A

I

atoms

A

J

) =

G

(

h

α

i

atoms

A

I

G

h

α

i

atoms

A

J

) =

G

h

α

i

atoms

A

I

t

G

h

α

i

atoms

A

J

=

α

0

I

t

α

0

J.

Let continue

α

0

till a funcoid f (by the theorem

595

):

h

f

iX

=

d

h

α

0

i

X

.

Let’s prove the reverse of (

8

):

l

DG

◦h

α

i

atoms

◦ ↑

A

E

a

=

l

DG

◦h

α

i

E

h

atoms

i

A

a

v

l

DG

◦h

α

i

E

{{

a

}}

=

l

nG

◦h

α

i

{

a

}

o

=

l

nG

h

α

i

{

a

}

o

=

l

nG

{

αa

}

o

=

l

{{

αa

}}

=

αa.

Finally,

αa

=

l

DG

◦h

α

i

atoms

◦ ↑

A

E

a

=

l

h

α

0

i

a

=

h

f

i

a,

so

h

f

i

is a continuation of

α

.

2

Consider the relation

δ

0

P

(

P

A

×

P

B

) defined by the formula (for every

X

P

A

,

Y

P

B

)

X δ

0

Y

⇔ ∃

x

atoms

A

X, y

atoms

A

Y

:

x δ y.

Obviously

¬

(

X δ

0

) and

¬

(

δ

0

Y

).

For suitable

I

and

J

we have:

I

J δ

0

Y

x

atoms

A

(

I

J

)

, y

atoms

B

Y

:

x δ y

x

atoms

A

I

atoms

A

J, y

atoms

B

Y

:

x δ y

x

atoms

A

I, y

atoms

B

Y

:

x δ y

∨ ∃

x

atoms

A

J, y

atoms

B

Y

:

x δ y

I δ

0

Y

J δ

0

Y

;