theorem Th9: :: NORMFORM:9

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