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