theorem :: REWRITE1:41

for R being Relation
for a, b being object st a,b are_divergent_wrt R holds
b,a are_divergent_wrt R ;