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