theorem Th26: :: REWRITE1:26

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