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