theorem Th12: :: NORMFORM:12

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