let L be B_Lattice; :: thesis: for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y & X misses X ` & Y misses Y ` holds

( X = Y ` & Y = X ` )

let X, Y be Element of L; :: thesis: ( (X `) "\/" (Y `) = X "\/" Y & X misses X ` & Y misses Y ` implies ( X = Y ` & Y = X ` ) )

assume that

A1: (X `) "\/" (Y `) = X "\/" Y and

A2: X misses X ` and

A3: Y misses Y ` ; :: thesis: ( X = Y ` & Y = X ` )

A4: X "/\" (X `) = Bottom L by A2;

A5: Y "/\" (Y `) = Bottom L by A3;

then A6: (Y `) "/\" ((X `) "\/" (Y `)) = ((Y `) "/\" X) "\/" (Bottom L) by A1, LATTICES:def 11;

(Y "/\" (X `)) "\/" (Y "/\" (Y `)) = Y "/\" (X "\/" Y) by A1, LATTICES:def 11;

then Y "/\" (X `) = Y "/\" (X "\/" Y) by A5;

then A7: Y "/\" (X `) = Y by LATTICES:def 9;

(X "/\" (X `)) "\/" (X "/\" (Y `)) = X "/\" (X "\/" Y) by A1, LATTICES:def 11;

then X "/\" (Y `) = X "/\" (X "\/" Y) by A4

.= X by LATTICES:def 9 ;

hence X = Y ` by A6, LATTICES:def 9; :: thesis: Y = X `

(X `) "/\" ((X `) "\/" (Y `)) = (Bottom L) "\/" ((X `) "/\" Y) by A1, A4, LATTICES:def 11;

hence Y = X ` by A7, LATTICES:def 9; :: thesis: verum

( X = Y ` & Y = X ` )

let X, Y be Element of L; :: thesis: ( (X `) "\/" (Y `) = X "\/" Y & X misses X ` & Y misses Y ` implies ( X = Y ` & Y = X ` ) )

assume that

A1: (X `) "\/" (Y `) = X "\/" Y and

A2: X misses X ` and

A3: Y misses Y ` ; :: thesis: ( X = Y ` & Y = X ` )

A4: X "/\" (X `) = Bottom L by A2;

A5: Y "/\" (Y `) = Bottom L by A3;

then A6: (Y `) "/\" ((X `) "\/" (Y `)) = ((Y `) "/\" X) "\/" (Bottom L) by A1, LATTICES:def 11;

(Y "/\" (X `)) "\/" (Y "/\" (Y `)) = Y "/\" (X "\/" Y) by A1, LATTICES:def 11;

then Y "/\" (X `) = Y "/\" (X "\/" Y) by A5;

then A7: Y "/\" (X `) = Y by LATTICES:def 9;

(X "/\" (X `)) "\/" (X "/\" (Y `)) = X "/\" (X "\/" Y) by A1, LATTICES:def 11;

then X "/\" (Y `) = X "/\" (X "\/" Y) by A4

.= X by LATTICES:def 9 ;

hence X = Y ` by A6, LATTICES:def 9; :: thesis: Y = X `

(X `) "/\" ((X `) "\/" (Y `)) = (Bottom L) "\/" ((X `) "/\" Y) by A1, A4, LATTICES:def 11;

hence Y = X ` by A7, LATTICES:def 9; :: thesis: verum