let L be B_Lattice; :: thesis: for X, Y being Element of L holds X "\/" Y = X \+\ (Y \ X)
let X, Y be Element of L; :: thesis: X "\/" Y = X \+\ (Y \ X)
X "\/" Y = (X "\/" Y) "/\" (Top L) by LATTICES:43
.= (X "\/" Y) "/\" (X "\/" (X `)) by LATTICES:48
.= X "\/" (Y "/\" (X `)) by LATTICES:31
.= (((Y `) "/\" X) "\/" X) "\/" (Y "/\" (X `)) by LATTICES:def 8
.= ((X "/\" (Y `)) "\/" (X "/\" X)) "\/" (Y "/\" (X `)) by LATTICES:18
.= ((X "/\" (Y `)) "\/" (X "/\" X)) "\/" (Y "/\" ((X `) "/\" (X `))) by LATTICES:18
.= ((X "/\" (Y `)) "\/" (X "/\" ((X `) `))) "\/" (Y "/\" ((X `) "/\" (X `))) by LATTICES:49
.= (X "/\" ((Y `) "\/" ((X `) `))) "\/" (Y "/\" ((X `) "/\" (X `))) by LATTICES:def 11
.= (X "/\" ((Y "/\" (X `)) `)) "\/" (Y "/\" ((X `) "/\" (X `))) by LATTICES:50
.= X \+\ (Y \ X) by LATTICES:def 7 ;
hence X "\/" Y = X \+\ (Y \ X) ; :: thesis: verum