theorem :: BOOLEALG:21

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