theorem Th45: :: BOOLEALG:45

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