let L be B_Lattice; :: thesis: for X, Y being Element of L holds X "\/" (Y \ X) = X "\/" Y
let X, Y be Element of L; :: thesis: X "\/" (Y \ X) = X "\/" Y
X "\/" (Y \ X) = (X "\/" Y) "/\" (X "\/" (X `)) by LATTICES:11
.= (X "\/" Y) "/\" (Top L) by LATTICES:21 ;
hence X "\/" (Y \ X) = X "\/" Y ; :: thesis: verum