theorem Th30: :: REWRITE1:30

for R being Relation
for a, b, c being object st a,b are_convertible_wrt R & b,c are_convertible_wrt R holds
a,c are_convertible_wrt R by Th16;