let A, B be non empty preBoolean set ; :: thesis: for a, b being Element of [:A,B:] st a c= b & b c= a holds

a = b

let a, b be Element of [:A,B:]; :: thesis: ( a c= b & b c= a implies a = b )

assume ( a `1 c= b `1 & a `2 c= b `2 & b `1 c= a `1 & b `2 c= a `2 ) ; :: according to NORMFORM:def 1 :: thesis: a = b

then ( a `1 = b `1 & a `2 = b `2 ) ;

hence a = b by DOMAIN_1:2; :: thesis: verum

a = b

let a, b be Element of [:A,B:]; :: thesis: ( a c= b & b c= a implies a = b )

assume ( a `1 c= b `1 & a `2 c= b `2 & b `1 c= a `1 & b `2 c= a `2 ) ; :: according to NORMFORM:def 1 :: thesis: a = b

then ( a `1 = b `1 & a `2 = b `2 ) ;

hence a = b by DOMAIN_1:2; :: thesis: verum