19.6. SPECIFYING FUNCOIDS BY FUNCTIONS OR RELATIONS ON ATOMIC FILTERS295

Proof.

Existence of no more than one such funcoids and formulas (

25

and

(

27

follow from theorem

1542

and corollary

1544

and the fact that our filtrators

are separable.

1

Consider the function

α

0

B

Z

0

defined by the formula (for every

X

Z

0

)

α

0

X

=

l

h

α

i

atoms

A

X.

Obviously

α

0

Z

0

=

B

. For every

I, J

Z

0

α

0

(

I

t

J

) =

l

h

α

i

atoms

A

(

I

t

J

) =

l

h

α

i

(atoms

A

I

atoms

A

J

) =

l

(

h

α

i

atoms

A

I

∪ h

α

i

atoms

A

J

) =

l

h

α

i

atoms

A

I

t

l

h

α

i

atoms

A

J

=

α

0

I

t

α

0

J.

Let continue

α

0

till a pointfree funcoid

f

(by the theorem

1510

):

h

f

iX

=

d

h

α

0

i

up

Z

0

X

.

Let’s prove the reverse of (

24

):

l

D

l

◦h

α

i

atoms

A

E

up

Z

0

a

=

l

D

l

◦h

α

i

E

atoms

A

up

Z

0

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

A

E

up

Z

0

a

=

l

h

α

0

i

up

Z

0

a

=

h

f

i

a,

so

h

f

i

is a continuation of

α

.

2

Consider the relation

δ

0

P

(

Z

0

×

Z

1

) defined by the formula (for every

X

Z

0

,

Y

Z

1

)

X δ

0

Y

⇔ ∃

x

atoms

A

X, y

atoms

B

Y

:

x δ y.

Obviously

¬

(

X δ

0

Z

1

) and

¬

(

Z

0

δ

0

Y

).

I

t

J δ

0

Y

x

atoms

A

(

I

t

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

;