let R be Relation; :: thesis: for a, b being object st a,b are_convertible_wrt R & a <> b holds
( a in field R & b in field R )
let a, b be object ; :: thesis: ( a,b are_convertible_wrt R & a <> b implies ( a in field R & b in field R ) )
A1: field (R \/ (R ~)) = (field R) \/ (field (R ~)) by RELAT_1:18
.= (field R) \/ (field R) by RELAT_1:21
.= field R ;
assume R \/ (R ~) reduces a,b ; :: according to REWRITE1:def 4 :: thesis: ( not a <> b or ( a in field R & b in field R ) )
hence ( not a <> b or ( a in field R & b in field R ) ) by A1, Th18; :: thesis: verum