let L be B_Lattice; :: thesis: for X, Y, Z being Element of L holds X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)

let X, Y, Z be Element of L; :: thesis: X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)

X \ (Y \+\ Z) = X \ ((Y "\/" Z) \ (Y "/\" Z)) by Th64

.= (X \ (Y "\/" Z)) "\/" (X "/\" (Y "/\" Z)) by Th37

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

hence X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z) ; :: thesis: verum

let X, Y, Z be Element of L; :: thesis: X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z)

X \ (Y \+\ Z) = X \ ((Y "\/" Z) \ (Y "/\" Z)) by Th64

.= (X \ (Y "\/" Z)) "\/" (X "/\" (Y "/\" Z)) by Th37

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

hence X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" ((X "/\" Y) "/\" Z) ; :: thesis: verum