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:23
.= ((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:20
.= (Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" (Bottom L)) by LATTICES:20
.= (X \ Y) "\/" (Y \ X) ;
hence (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X) ; :: thesis: verum