theorem :: NORMFORM:13

for A, B being non empty preBoolean set
for a, b being Element of [:A,B:] holds (a \ b) \/ b = a \/ b