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