theorem Th55: :: REWRITE1:55

for R being weakly-normalizing with_UN_property Relation
for a, b being object st a,b are_convertible_wrt R holds
nf (a,R) = nf (b,R)