let R be Relation; :: thesis: for a, b being set st a,b are_convertible_wrt R & not a in field R holds
a = b
let a, b be set ; :: thesis: ( a,b are_convertible_wrt R & not a in field R implies a = b )
A1: ( field R = field (R ~ ) & field (R \/ (R ~ )) = (field R) \/ (field (R ~ )) ) by RELAT_1:33, RELAT_1:38;
assume R \/ (R ~ ) reduces a,b ; :: according to REWRITE1:def 4 :: thesis: ( a in field R or a = b )
hence ( a in field R or a = b ) by A1, Th15; :: thesis: verum