let R be Relation; :: thesis: for a, b being object 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 object ; :: 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 object such that
A2: ( R reduces a,c & R reduces b,c ) ;
( a,c are_convertible_wrt R & c,b are_convertible_wrt R ) by A2, Th25;
hence a,b are_convertible_wrt R by Th30; :: thesis: verum

end;

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

then consider c being object such that
A3: ( R reduces c,a & R reduces c,b ) ;
( c,b are_convertible_wrt R & a,c are_convertible_wrt R ) by A3, Th25;
hence a,b are_convertible_wrt R by Th30; :: thesis: verum

end;

end;