theorem :: REWRITE1:31

for R being Relation
for a, b being object st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R by Lm5;