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:23
.= X "/\" ((Y `) "\/" Z)
.= (X "/\" (Y `)) "\/" (X "/\" Z) by LATTICES:def 11 ;
hence X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z) ; :: thesis: verum