2.

(

a

u

b

)

(

D a

)

=

G

f

c

2

Da

j

c

u

a

u

b

= 0

g

=

G

f

c

2

A

j

c

v

a

^

c

u

a

u

b

= 0

g

=

G

f

c

2

A

j

c

v

a

^

c

u

b

= 0

g

=

a

#

b:

Proposition 3.42.

(

a

t

b

)

n

b

v

a

for an arbitrary complete lattice.

Proof.

(

a

t

b

)

n

b

=

d

f

z

2

A

j

a

t

b

v

b

t

z

g

.

But

a

v

z

)

a

t

b

v

b

t

z

. So

f

z

2

A

j

a

t

b

v

b

t

z

g  f

z

2

A

j

a

v

z

g

.

Consequently,

(

a

t

b

)

n

b

v

d

f

z

2

A

j

a

v

z

g

=

a

.

3.4 Several equal ways to express pseudodierence

Theorem 3.43.

For an atomistic co-brouwerian lattice

A

and

a; b

2

A

the following expressions

are always equal:

1.

a

n

b

=

d

f

z

2

A

j

a

v

b

t

z

g

(quasidierence of

a

and

b

);

2.

a

#

b

=

F

f

z

2

A

j

z

v

a

^

z

u

b

= 0

g

(second quasidierence of

a

and

b

);

3.

F

(

atoms

a

n

atoms

b

)

.

Proof.

Proof of (1)

=

(3):

a

n

b

=

¡G

atoms

a

n

b

=

(theorem

2.123

)

G

f

A

n

b

j

A

2

atoms

a

g

=

A

if

A

2

/

atoms

b

0

if

A

2

atoms

b

j

A

2

atoms

a

=

G

f

A

j

A

2

atoms

a; A

2

/

atoms

b

g

=

G

(

atoms

a

n

atoms

b

)

:

Proof of (2)

=

(3):

a

n

b

is dened because our lattice is co-brouwerian. Taking the above into account, we have

a

n

b

=

G

(

atoms

a

n

atoms

b

) =

G

f

z

2

atoms

a

j

z

u

b

= 0

A

g

:

So

F

f

z

2

atoms

a

j

z

u

b

= 0

A

g

is dened.

If

z

v

a

^

z

u

b

= 0

A

then

z

0

=

F

f

x

2

atoms

z

j

x

u

b

= 0

A

g

is dened.

z

0

is a lower bound for

f

z

2

atoms

a

j

z

u

b

= 0

A

g

.

Thus

z

0

2 f

z

2

A

j

z

v

a

^

z

u

b

= 0

A

g

and so

F

f

z

2

atoms

a

j

z

u

b

= 0

A

g

is an upper bound of

f

z

2

A

j

z

v

a

^

z

u

b

= 0

A

g

.

If

y

is above every

z

0

2 f

z

2

A

j

z

v

a

^

z

u

b

= 0

A

g

then

y

is above every

z

2

atoms

a

such that

z

u

b

= 0

A

and thus

y

is above

F

f

z

2

atoms

a

j

z

u

b

= 0

A

g

.

Thus

F

f

z

2

atoms

a

j

z

u

b

= 0

A

g

is least upper bound of

f

z

2

A

j

z

v

a

^

z

u

b

= 0

A

g

;

3.4 Several equal ways to express pseudodifference

39