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) \ (X "/\" Z) = ((X "/\" Y) \ X) "\/" ((X "/\" Y) \ Z) by Th42
.= (Bottom L) "\/" ((X "/\" Y) \ Z) by Th29, LATTICES:6
.= (X "/\" Y) \ Z ;
hence X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z) by LATTICES:def 7; :: thesis: verum