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 = (Y \ X) "\/" X by Th52
.= (Y \ X) "\/" ((X \ Y) "\/" (X "/\" Y)) by Th53
.= (X \+\ Y) "\/" (X "/\" Y) by LATTICES:def 5 ; :: thesis: verum