theorem Th27: :: REWRITE1:27

for a, b being object st a,b are_convertible_wrt {} holds
a = b by Th13;