theorem :: REWRITE1:64

for R being Relation
for Q being complete Relation st R,Q are_equivalent holds
Q is Completion of R