let L be B_Lattice; :: thesis: for X, Y being Element of L st X \ Y = Y \ X holds
X = Y
let X, Y be Element of L; :: thesis: ( X \ Y = Y \ X implies X = Y )
assume A1: X \ Y = Y \ X ; :: thesis: X = Y
then (X "/\" (Y ` )) "/\" X = Y "/\" ((X ` ) "/\" X) by LATTICES:def 7
.= Y "/\" (Bottom L) by LATTICES:47
.= Bottom L by LATTICES:40 ;
then (X "/\" X) "/\" (Y ` ) = Bottom L by LATTICES:def 7;
then X "/\" (Y ` ) = Bottom L by LATTICES:18;
then (X "/\" (Y ` )) "\/" (X ` ) = (X "/\" (X ` )) "\/" (X ` ) by LATTICES:47
.= X ` by LATTICES:def 8 ;
then (X "\/" (X ` )) "/\" ((Y ` ) "\/" (X ` )) = X ` by LATTICES:31;
then (Top L) "/\" ((Y ` ) "\/" (X ` )) = X ` by LATTICES:48;
then (Y ` ) "\/" (X ` ) = X ` by LATTICES:43;
then (Y ` ) "/\" (X ` ) = Y ` by LATTICES:def 9;
then Y ` [= X ` by LATTICES:21;
then (X ` ) ` [= (Y ` ) ` by LATTICES:53;
then X [= (Y ` ) ` by LATTICES:49;
then A2: X [= Y by LATTICES:49;
X "/\" ((Y ` ) "/\" Y) = (Y "/\" (X ` )) "/\" Y by A1, LATTICES:def 7;
then X "/\" (Bottom L) = (Y "/\" (X ` )) "/\" Y by LATTICES:47;
then Bottom L = ((X ` ) "/\" Y) "/\" Y by LATTICES:40
.= (X ` ) "/\" (Y "/\" Y) by LATTICES:def 7
.= (X ` ) "/\" Y by LATTICES:18 ;
then X ` [= Y ` by LATTICES:52;
then (Y ` ) ` [= (X ` ) ` by LATTICES:53;
then Y [= (X ` ) ` by LATTICES:49;
then Y [= X by LATTICES:49;
hence X = Y by A2, Def3; :: thesis: verum