theorem :: BOOLEALG:28

for L being B_Lattice
for X, Y being Element of L st X [= Y holds
Y = X "\/" (Y \ X)