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