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