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, Def4;
A5: Y "/\" (Y `) = Bottom L by A3, Def4;
then (Y `) "/\" ((X `) "\/" (Y `)) = ((Y `) "/\" X) "\/" (Bottom L) by A1, LATTICES:def 11;
then A6: (Y `) "/\" ((X `) "\/" (Y `)) = (Y `) "/\" X by LATTICES:14;
(Y "/\" (X `)) "\/" (Y "/\" (Y `)) = Y "/\" (X "\/" Y) by A1, LATTICES:def 11;
then Y "/\" (X `) = Y "/\" (X "\/" Y) by A5, LATTICES:14;
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, LATTICES:14
.= 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;
then (X `) "/\" ((X `) "\/" (Y `)) = (X `) "/\" Y by LATTICES:14;
hence Y = X ` by A7, LATTICES:def 9; :: thesis: verum