let A, B be non empty preBoolean set ; :: thesis: for a, c, b being Element of [:A,B:] st a c= c & b c= c holds
a \/ b c= c
let a, c, b be Element of [:A,B:]; :: thesis: ( a c= c & b c= c implies a \/ b c= c )
assume ( a `1 c= c `1 & a `2 c= c `2 & b `1 c= c `1 & b `2 c= c `2 ) ; :: according to NORMFORM:def 1 :: thesis: a \/ b c= c
then ( (a `1 ) \/ (b `1 ) c= c `1 & (a `2 ) \/ (b `2 ) c= c `2 ) by XBOOLE_1:8;
hence ( (a \/ b) `1 c= c `1 & (a \/ b) `2 c= c `2 ) by MCART_1:7; :: according to NORMFORM:def 1 :: thesis: verum