let R be Relation; 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 ; ( ( 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 )
; a,b are_convertible_wrt R