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