let R be Relation; :: thesis: for a, b being object st a,b are_convertible_wrt R & not a in field R holds
a = b
let a, b be object ; :: 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:18, RELAT_1:21;
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, Th14; :: thesis: verum