for R being 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