theorem :: REWRITE1:65

for R being Relation
for C being Completion of R
for a, b being object holds
( a,b are_convertible_wrt R iff nf (a,C) = nf (b,C) )