 Let's denote

W

=

y

u

Dst

f

h

f

i

X

j

X

2

up

(

Src

f

;

Z

0

)

x

. We will prove that

W

is a generalized lter

base over

Z

1

. To prove this enough to show that

V

=

h

f

i

X

j

X

2

up

(

Src

f

;

Z

0

)

x

is a generalized

lter base.

Let

P

;

Q 2

V

. Then

P

=

h

f

i

A

,

Q

=

h

f

i

B

where

A; B

2

up

(

Src

f

;

Z

0

)

x

;

A

u

Z

0

B

2

up

(

Src

f

;

Z

0

)

x

(used the fact that it is a nitely meet-closed and theorem

4.44

and

R v P u

Dst

f

Q

for

R

=

h

f

i

(

A

u

Z

0

B

)

2

V

because Dst

f

is separable by obvious

4.136

So

V

is a generalized lter base and

thus

W

is a generalized lter base.

0

Dst

f

2

/

W

,

d

Dst

f

W

3

/ 0

Dst

f

by theorem

4.121

That is

8

X

2

up

(

Src

f

;

Z

0

)

x

:

y

u

Dst

f

h

f

i

X

=

/ 0

Dst

f

,

y

u

Dst

f

l

Dst

f

hh

f

ii

up

(

Src

f

;

Z

0

)

x

=

/ 0

Dst

f

:

Comparing with the above,

y

u

Dst

f

h

f

i

x

=

/ 0

Dst

f

,

y

u

Dst

f

d

Dst

f

hh

f

ii

up

(

Src

f

;

Z

0

)

x

=

/ 0

Dst

f

. So

h

f

i

x

=

d

Dst

f

hh

f

ii

up

(

Src

f

;

Z

0

)

x

because Dst

f

is separable (obvious

4.136

and the fact that

Z

1

is a

boolean lattice).

Theorem 15.26.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

be primary ltrators over boolean lattices.

1. A function

2

B

Z

0

conforming to the formulas (for every

I ; J

2

Z

0

)

0

Z

0

= 0

B

;

(

I

t

J

) =

I

t

J

can be continued to the function

h

f

i

for a unique

f

2

FCD

(

A

;

B

)

;

h

f

iX

=

l

B

h

i

up

(

A

;

Z

0

)

X

(15.1)

for every

X 2

A

.

2. A relation

2

P

(

Z

0

Z

1

)

conforming to the formulas (for every

I ; J ; K

2

Z

0

and

I

0

; J

0

;

K

0

2

Z

1

)

:

(0

Z

0

I

0

)

; I

t

J  K

0

,

I  K

0

_

J  K

0

;

:

(

0

Z

1

)

; K  I

0

t

J

0

,

K  I

0

_

K  J

0

(15.2)

can be continued to the relation

[

f

]

for a unique

f

2

FCD

(

A

;

B

)

;

X

[

f

]

Y , 8

X

2

up

(

A

;

Z

0

)

X

; Y

2

up

(

B

;

Z

1

)

Y

:

X  Y

(15.3)

for every

X 2

A

,

Y 2

B

.

Proof.

Existence of no more than one such pointfree funcoids and formulas (

15.1

and (

15.3

follow

from two previous theorems.

2.

f

Y

2

Z

1

j

X  Y

g

is obviously a free star for every

X

2

Z

0

. By properties of lters on boolean

lattices, there exist a unique lter

X

such that

@

(

X

) =

f

Y

2

Z

1

j

X  Y

g

for every

X

2

Z

0

.

Thus

2

B

Z

0

. Similarly it can be dened

2

A

Z

1

by the formula

@

(

Y

) =

f

X

2

Z

0

j

X  Y

g

. Let's

continue the functions

and

to

0

2

B

A

and

0

2

A

B

by the formulas

0

X

=

l

B

h

i

up

(

A

;

Z

0

)

X

and

0

Y

=

l

A

h

i

up

(

B

;

Z

1

)

Y

and

to

0

2

P

(

A

B

)

by the formula

X

0

Y , 8

X

2

up

(

A

;

Z

0

)

X

; Y

2

up

(

B

;

Z

1

)

Y

:

X  Y :

Y u

0

X

=

/ 0

B

, Y u

d

h

i

up

(

A

;

Z

0

)

X

=

/ 0

B

,

d

hY u ih

i

up

(

A

;

Z

0

)

X

=

/ 0

B

. Let's prove that

W

=

hY u ih

i

up

(

A

;

Z

0

)

X

is a generalized lter base: To prove it is enough to show that

h

i

up

(

A

;

Z

0

)

X

is a generalized lter

base.

If

A

;

B 2 h

i

up

(

A

;

Z

0

)

X

then exist

X

1

; X

2

2

up

(

A

;

Z

0

)

X

such that

A

=

X

1

and

B

=

X

2

.

Then

(

X

1

u

Z

0

X

2

)

2 h

i

up

(

A

;

Z

0

)

X

. So

h

i

up

(

A

;

Z

0

)

X

is a generalized lter base and thus

W

is a

generalized lter base.

180

Pointfree funcoids