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