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