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

1

Consider the function

α

0

F

(

B

)

T

A

defined by the formula (for every

X

T

A

)

α

0

X

=

l

h

α

i

atoms

X.

Obviously

α

0

T

A

=

F

(

B

)

. For every

I, J

T

A

α

0

(

I

t

J

) =

l

h

α

i

atoms

(

I

t

J

) =

l

h

α

i

(atoms

↑ ∪

atoms

J

) =

l

(

h

α

i

atoms

I

∪ h

α

i

atoms

J

) =

l

h

α

i

atoms

I

t

l

h

α

i

atoms

J

=

α

0

I

t

α

0

J.

Let continue

α

0

till a funcoid

f

(by the theorem

831

):

h

f

iX

=

d

h

α

0

i

up

X

.

Let’s prove the reverse of (

10

):

l

D

l

◦h

α

i

atoms

◦ ↑

E

up

a

=

l

D

l

◦h

α

i

E

h

atoms

i

h↑i

up

a

v

l

D

l

◦h

α

i

E

{{

a

}}

=

l

n

l

◦h

α

i

{

a

}

o

=

l

n

l

h

α

i

{

a

}

o

=

l

n

l

{

αa

}

o

=

l

{

αa

}

=

αa.

Finally,

αa

=

l

D

l

◦h

α

i

atoms

◦ ↑

E

up

a

=

l

h

α

0

i

up

a

=

h

f

i

a,

so

h

f

i

is a continuation of

α

.

2

Consider the relation

δ

0

P

(

T

A

×

T

B

) defined by the formula (for every

X

T

A

,

Y

T

B

)

X δ

0

Y

⇔ ∃

x

atoms

X, y

atoms

Y

:

x δ y.

Obviously

¬

(

X δ

0

F

(

B

)

) and

¬

(

F

(

A

)

δ

0

Y

).

For suitable

I

and

J

we have:

I

t

J δ

0

Y

x

atoms

(

I

t

J

)

, y

atoms

Y

:

x δ y

x

atoms

I

atoms

J, y

atoms

Y

:

x δ y

x

atoms

I, y

atoms

Y

:

x δ y

∨ ∃

x

atoms

J, y

atoms

Y

:

x δ y

I δ

0

Y

J δ

0

Y

;

similarly

X δ

0

I

t

J

X δ

0

I

X δ

0

J

for suitable

I

and

J

. Let’s continue

δ

0

till a

funcoid

f

(by the theorem

831

):

X

[

f

]

Y ⇔ ∀

X

up

X

, Y

up

Y

:

X δ

0

Y.