theorem :: NORMFORM:15

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