let R be Relation; :: thesis: for Q being complete Relation st R,Q are_equivalent holds
Q is Completion of R
let Q be complete Relation; :: thesis: ( R,Q are_equivalent implies Q is Completion of R )
assume A1: for a, b being set holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q ) ; :: according to REWRITE1:def 26 :: thesis: Q is Completion of R
let a, b be set ; :: according to REWRITE1:def 28 :: thesis: ( 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, Th38; :: thesis: verum