let R be Relation; for Q being complete Relation st R,Q are_equivalent holds
Q is Completion of R
let Q be complete Relation; ( R,Q are_equivalent implies Q is Completion of R )
assume A1:
for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q )
; REWRITE1:def 26 Q is Completion of R
let a, b be object ; REWRITE1:def 28 ( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q )
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q )
by A1;
hence
( a,b are_convertible_wrt R iff a,b are_convergent_wrt Q )
by Def23, Th37; verum