theorem Th59: :: REWRITE1:59

for R being Relation
for a, b being object st a,b are_critical_wrt R holds
a,b are_convertible_wrt R by Th37, Th45;