let L be B_Lattice; :: thesis: for X, Y being Element of L holds (X "\/" Y) \ (X \+\ Y) = X "/\" Y
let X, Y be Element of L; :: thesis: (X "\/" Y) \ (X \+\ Y) = X "/\" Y
set XY = X "\/" Y;
thus (X "\/" Y) \ (X \+\ Y) = (X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `)) by LATTICES:51
.= (X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y `) "\/" ((X `) `))) by LATTICES:50
.= (X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `))) by LATTICES:50
.= (X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" X)) by LATTICES:49
.= (X "\/" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X)) by LATTICES:49
.= ((X "\/" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X) by LATTICES:def 7
.= (((X "\/" Y) "/\" (X `)) "\/" ((X "\/" Y) "/\" Y)) "/\" ((Y `) "\/" X) by LATTICES:def 11
.= (((X "\/" Y) "/\" (X `)) "\/" Y) "/\" ((Y `) "\/" X) by LATTICES:def 9
.= (((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" Y) "/\" ((Y `) "\/" X) by LATTICES:def 11
.= (((Bottom L) "\/" (Y "/\" (X `))) "\/" Y) "/\" ((Y `) "\/" X) by LATTICES:47
.= ((Y "/\" (X `)) "\/" Y) "/\" ((Y `) "\/" X) by LATTICES:39
.= Y "/\" ((Y `) "\/" X) by LATTICES:def 8
.= (Y "/\" (Y `)) "\/" (Y "/\" X) by LATTICES:def 11
.= (Bottom L) "\/" (Y "/\" X) by LATTICES:47
.= X "/\" Y by LATTICES:39 ; :: thesis: verum