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)
.= (X "\/" Y) "/\" (X "\/" (X `)) by LATTICES:21
.= X "\/" (Y "/\" (X `)) by LATTICES:11
.= ((X "/\" (Y `)) "\/" (X "/\" X)) "\/" (Y "/\" (X `)) by LATTICES:def 8
.= ((X "/\" (Y `)) "\/" (X "/\" ((X `) `))) "\/" (Y "/\" ((X `) "/\" (X `)))
.= (X "/\" ((Y `) "\/" ((X `) `))) "\/" (Y "/\" ((X `) "/\" (X `))) by LATTICES:def 11
.= (X "/\" ((Y "/\" (X `)) `)) "\/" (Y "/\" ((X `) "/\" (X `))) by LATTICES:23
.= X \+\ (Y \ X) by LATTICES:def 7 ;
hence X "\/" Y = X \+\ (Y \ X) ; :: thesis: verum