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