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