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