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

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

thus X \+\ Y = (X \ (X "/\" Y)) "\/" (Y \ X) by Th33

.= (X \ (X "/\" Y)) "\/" (Y \ (X "/\" Y)) by Th33

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

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

thus X \+\ Y = (X \ (X "/\" Y)) "\/" (Y \ X) by Th33

.= (X \ (X "/\" Y)) "\/" (Y \ (X "/\" Y)) by Th33

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