 If

z

a

z

F

b

= 0

A

then

z

0

=

x

atoms

z

|

x

A

b

= 0

A

is defined.

z

0

is a lower bound for

z

atoms

a

|

z

A

b

= 0

A

.

Thus

z

0

z

A

|

z

a

z

A

b

= 0

A

and so

z

atoms

a

|

z

A

b

= 0

A

is an upper bound of

z

A

|

z

a

z

A

b

= 0

A

.

If

y

is above every

z

0

z

A

|

z

a

z

A

b

= 0

A

then

y

is above every

z

atoms

a

such that

z

A

b

= 0

A

and thus

y

is above

z

atoms

a

|

z

A

b

= 0

A

.

Thus

z

atoms

a

|

z

A

b

= 0

A

is least upper bound of

z

A

|

z

a

z

A

b

= 0

A

,

that is

z

A

|

z

a

z

A

b

= 0

A

=

z

atoms

a

|

z

A

b

= 0

A

=

[

(atoms

a

\

atoms

b

)

.

2

Note that

F

is co-brouwerian by corollary 11 in  and atomistic by theorem

48 in , so our theorem applies to the lattice

F

, and more generally to any

filters on a boolean lattice.

Proposition 1

For filters on boolean lattices the three above ways to express

quasidifference of

a

and

b

are also equal to

S

F

{

a

F

B

|

B

up

b

}

(

X

denotes the principal filter induced by

X

).

Remark 1

By corollary 8 in  the set of filters on a boolean lattice is complete.

So our formula is well-defined.

Proof

Using results from :

S

F

{

z

F

|

z

a

z

b

= 0

F

} ⊆

S

F

{

a

F

B

|

B

up

b

}

because

z

∈ {

z

F

|

z

a

z

b

= 0

F

} ⇔

z

a

z

b

= 0

F

z

a

∧ ∃

B

up

b

:

z

∩ ↑

B

= 0

F

z

a

∧ ∃

B

up

b

:

z

⊆ ↑

B

B

up

b

: (

z

a

z

⊆ ↑

B

)

⇔ ∃

B

up

b

:

z

a

F

B

z

F

[

{

a

F

B

|

B

up

b

}

.

But obviously

a

F

B

∈ {

z

F

|

z

a

z

b

= 0

F

}

and thus

a

F

B

F

[

{

z

F

|

z

a

z

b

= 0

F

}

and so

S

F

{

z

F

|

z

a

z

b

= 0

F

} ⊇

S

F

{

a

F

B

|

B

up

b

}

.

2

The above proposition completes the proof of problem 1 in .

3