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