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 ` ) ` )) by LATTICES:50
.= X "/\" ((X ` ) "\/" Y) by LATTICES:49
.= (X "/\" (X ` )) "\/" (X "/\" Y) by LATTICES:def 11
.= (Bottom L) "\/" (X "/\" Y) by LATTICES:47 ;
hence X \ (X \ Y) = X "/\" Y by LATTICES:39; :: thesis: verum