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)
A1: X "/\" Y [= X by LATTICES:23;
(X "/\" Y) \ (X "/\" Z) = ((X "/\" Y) \ X) "\/" ((X "/\" Y) \ Z) by Th59
.= (Bottom L) "\/" ((X "/\" Y) \ Z) by A1, Th46
.= (X "/\" Y) \ Z by LATTICES:39 ;
hence X "/\" (Y \ Z) = (X "/\" Y) \ (X "/\" Z) by LATTICES:def 7; :: thesis: verum