theorem :: REWRITE1:63

for R being Relation
for C being Completion of R holds R,C are_equivalent