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;
A3: ( a,c are_convertible_wrt R & b,c are_convertible_wrt R ) by A2, Th26;
c,b are_convertible_wrt R by A2, Th26;
hence a,b are_convertible_wrt R by A3, 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
A4: ( R reduces c,a & R reduces c,b ) by Def8;
A5: ( c,a are_convertible_wrt R & c,b are_convertible_wrt R ) by A4, Th26;
a,c are_convertible_wrt R by A4, Th26;
hence a,b are_convertible_wrt R by A5, Th31; :: thesis: verum

end;

end;