 Proof.

Existence of no more than one such funcoids and formulas (

15.6

and (

15.8

follow from

the theorem

6.65

and corollary

15.24

and the fact that our ltrators are with separable core.

1. Consider the function

0

2

B

Z

0

dened by the formula (for every

X

2

Z

0

)

0

X

=

G

h

i

atoms

A

X:

Obviously

0

0

Z

0

= 0

B

. For every

I ; J

2

Z

0

0

(

I

t

J

) =

G

h

i

atoms

A

(

I

t

J

)

=

G

h

i

(

atoms

A

I

[

atoms

A

J

)

=

G

(

h

i

atoms

A

I

[ 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 pointfree funcoid

f

(by the theorem

15.26

):

h

f

iX

=

d

h

0

i

up

(

A

;

Z

0

)

X

.

Let's prove the reverse of (

15.5

):

l

G

h

atoms

A

up

(

A

;

Z

0

)

a

=

l

G

h

i

h

atoms

A

i

up

(

A

;

Z

0

)

a

v

l

G

h

i

ff

a

gg

=

l

¡G

h

i

f

a

g

=

l

G

h

if

a

g

=

l

G

f

a

g

=

l

f

a

g

=

a:

Finally,

a

=

l

G

h

atoms

A

up

(

A

;

Z

0

)

a

=

l

h

0

i

up

(

A

;

Z

0

)

a

=

h

f

i

a;

so

h

f

i

is a continuation of

.

2. Consider the relation

0

2

P

(

Z

0

Z

1

)

dened by the formula (for every

X

2

Z

0

,

Y

2

Z

1

)

0

Y

, 9

x

2

atoms

A

X ; y

2

atoms

B

Y

:

x  y:

Obviously

:

(

0

0

Z

1

)

and

:

(0

Z

0

0

Y

)

.

I

t

0

Y

, 9

x

2

atoms

A

(

I

t

J

)

; y

2

atoms

B

Y

:

x  y

, 9

x

2

atoms

A

I

[

atoms

A

J ; y

2

atoms

B

Y

:

x  y

, 9

x

2

atoms

A

I ; y

2

atoms

B

Y

:

x  y

_ 9

x

2

atoms

A

J ; y

2

atoms

B

Y

:

x  y

,

0

Y

_

0

Y

;

similarly

0

I

t

J

,

0

I

_

0

J

. Let's continue

0

till a funcoid

f

(by the theorem

15.26

):

X

[

f

]

Y , 8

X

2

up

(

A

;

Z

0

)

X

; Y

2

up

(

B

;

Z

1

)

Y

:

0

Y :

The reverse of (

15.7

implication is trivial, so

8

X

2

up

(

A

;

Z

0

)

a; Y

2

up

(

B

;

Z

1

)

b

9

x

2

atoms

A

X ; y

2

atoms

B

Y

:

x  y

,

a  b:

8

X

2

up

(

A

;

Z

0

)

a; Y

2

up

(

B

;

Z

1

)

b

9

x

2

atoms

A

X ; y

2

atoms

B

Y

:

x  y

, 8

X

2

up

(

A

;

Z

0

)

a; Y

2

up

(

B

;

Z

1

)

b

:

0

Y

,

a

[

f

]

b

.

So

a  b

,

a

[

f

]

b

, that is

[

f

]

is a continuation of

.

Theorem 15.59.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices. If

R

2

P

FCD

(

A

;

B

)

and

x

2

atoms

A

,

y

2

atoms

B

, then

1.

h

d

R

i

x

=

d

fh

f

i

x

j

f

2

R

g

;

2.

x

[

d

R

]

y

, 8

f

2

R

:

x

[

f

]

y

.

Proof.

186

Pointfree funcoids