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 )
A1: ( (b \/ c) `1 = (b `1) \/ (c `1) & (b \/ c) `2 = (b `2) \/ (c `2) ) by MCART_1:7;
A2: ( (a \ c) `1 = (a `1) \ (c `1) & (a \ c) `2 = (a `2) \ (c `2) ) by MCART_1:7;
assume ( a `1 c= (b \/ c) `1 & a `2 c= (b \/ c) `2 ) ; :: according to NORMFORM:def 1 :: thesis: a \ c c= b
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