let R be Relation; :: thesis: for C being Completion of R holds R,C are_equivalent
let C be Completion of R; :: thesis: R,C are_equivalent
let a, b be object ; :: according to REWRITE1:def 26 :: thesis: ( a,b are_convertible_wrt R iff a,b are_convertible_wrt C )
( a,b are_convertible_wrt R iff a,b are_convergent_wrt C ) by Def28;
hence ( a,b are_convertible_wrt R iff a,b are_convertible_wrt C ) by Def23, Th37; :: thesis: verum