let L be B_Lattice; :: thesis: for X, Y, Z being Element of L holds X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z)
let X, Y, Z be Element of L; :: thesis: X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z)
X \ (Y \ Z) = X "/\" ((Y ` ) "\/" ((Z ` ) ` )) by LATTICES:50
.= X "/\" ((Y ` ) "\/" Z) by LATTICES:49
.= (X "/\" (Y ` )) "\/" (X "/\" Z) by LATTICES:def 11 ;
hence X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z) ; :: thesis: verum