for R being Relation
for a, b, c being object st ( ( R reduces b,a & b,c are_divergent_wrt R ) or ( a,b are_divergent_wrt R & R reduces b,c ) ) holds
a,c are_divergent_wrt R