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:20
.= Bottom L ;
then (X "/\" X) "/\" (Y `) = Bottom L by LATTICES:def 7;
then (X "/\" (Y `)) "\/" (X `) = (X "/\" (X `)) "\/" (X `) by LATTICES:20
.= X ` by LATTICES:def 8 ;
then (X "\/" (X `)) "/\" ((Y `) "\/" (X `)) = X ` by LATTICES:11;
then (Top L) "/\" ((Y `) "\/" (X `)) = X ` by LATTICES:21;
then (Y `) "/\" (X `) = Y ` by LATTICES:def 9;
then (X `) ` [= (Y `) ` by LATTICES:4, LATTICES:26;
then X [= (Y `) ` ;
then A2: X [= Y ;
X "/\" ((Y `) "/\" Y) = (Y "/\" (X `)) "/\" Y by A1, LATTICES:def 7;
then X "/\" (Bottom L) = (Y "/\" (X `)) "/\" Y by LATTICES:20;
then Bottom L = (X `) "/\" (Y "/\" Y) by LATTICES:def 7
.= (X `) "/\" Y ;
then Y [= (X `) ` by LATTICES:25;
then Y [= X ;
hence X = Y by A2; :: thesis: verum