for R being Relation
for a being object holds a,a are_convertible_wrt R by Th12;