for R being Relation st R is subcommutative holds
for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R