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 Th35

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

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

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

thus X "\/" Y = (Y \ X) "\/" X by Th35

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

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