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