theorem :: NORMFORM:14

for A, B being non empty preBoolean set
for a, b, c being Element of [:A,B:] st a \ b c= c holds
a c= b \/ c by XBOOLE_1:44;