let L be B_Lattice; :: thesis: for X, Y being Element of L holds (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)
let X, Y be Element of L; :: thesis: (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X)
(X "\/" Y) \ (X "/\" Y) = (X "\/" Y) "/\" ((X ` ) "\/" (Y ` )) by LATTICES:50
.= ((X "\/" Y) "/\" (X ` )) "\/" ((X "\/" Y) "/\" (Y ` )) by LATTICES:def 11
.= ((X "/\" (X ` )) "\/" (Y "/\" (X ` ))) "\/" ((X "\/" Y) "/\" (Y ` )) by LATTICES:def 11
.= ((X "/\" (X ` )) "\/" (Y "/\" (X ` ))) "\/" ((X "/\" (Y ` )) "\/" (Y "/\" (Y ` ))) by LATTICES:def 11
.= ((Bottom L) "\/" (Y "/\" (X ` ))) "\/" ((X "/\" (Y ` )) "\/" (Y "/\" (Y ` ))) by LATTICES:47
.= ((Bottom L) "\/" (Y "/\" (X ` ))) "\/" ((X "/\" (Y ` )) "\/" (Bottom L)) by LATTICES:47
.= (Y "/\" (X ` )) "\/" ((X "/\" (Y ` )) "\/" (Bottom L)) by LATTICES:39
.= (X \ Y) "\/" (Y \ X) by LATTICES:39 ;
hence (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X) ; :: thesis: verum