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:24

.= ((X "/\" X) "/\" (Y `)) "/\" (Z `) by LATTICES:def 7

.= (X "/\" (X "/\" (Y `))) "/\" (Z `) by LATTICES:def 7

.= (X \ Y) "/\" (X \ Z) by LATTICES:def 7 ; :: thesis: verum

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:24

.= ((X "/\" X) "/\" (Y `)) "/\" (Z `) by LATTICES:def 7

.= (X "/\" (X "/\" (Y `))) "/\" (Z `) by LATTICES:def 7

.= (X \ Y) "/\" (X \ Z) by LATTICES:def 7 ; :: thesis: verum