let R be Relation; :: thesis: for a, b being set st ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) holds
a,b are_convertible_wrt R
let a, b be set ; :: thesis: ( ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) implies a,b are_convertible_wrt R )
assume A1: ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) ; :: thesis: a,b are_convertible_wrt R

per cases ( a,b are_convergent_wrt R or a,b are_divergent_wrt R ) by A1;

suppose a,b are_convergent_wrt R ; :: thesis: a,b are_convertible_wrt R

then consider c being set such that
A2: ( R reduces a,c & R reduces b,c ) by Def7;
( a,c are_convertible_wrt R & c,b are_convertible_wrt R ) by A2, Th26;
hence a,b are_convertible_wrt R by Th31; :: thesis: verum

end;

suppose a,b are_divergent_wrt R ; :: thesis: a,b are_convertible_wrt R

then consider c being set such that
A3: ( R reduces c,a & R reduces c,b ) by Def8;
( c,b are_convertible_wrt R & a,c are_convertible_wrt R ) by A3, Th26;
hence a,b are_convertible_wrt R by Th31; :: thesis: verum

end;

end;