for R being Relation
for a, b being object st a,b are_convergent<=1_wrt R holds
a,b are_convergent_wrt R