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