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