let R be Relation; :: thesis: for C being Completion of R
for a, b being set holds
( a,b are_convertible_wrt R iff nf a,C = nf b,C )
let C be Completion of R; :: thesis: for a, b being set holds
( a,b are_convertible_wrt R iff nf a,C = nf b,C )
let a, b be set ; :: thesis: ( a,b are_convertible_wrt R iff nf a,C = nf b,C )
A1: ( a,b are_convertible_wrt R iff a,b are_convergent_wrt C ) by Def28;
( a,b are_convergent_wrt C implies a,b are_convertible_wrt C ) by Th38;
hence ( a,b are_convertible_wrt R implies nf a,C = nf b,C ) by Def28, Th56; :: thesis: ( nf a,C = nf b,C implies a,b are_convertible_wrt R )
( nf a,C is_a_normal_form_of a,C & nf b,C is_a_normal_form_of b,C ) by Th55;
then ( C reduces a, nf a,C & C reduces b, nf b,C ) by Def6;
hence ( nf a,C = nf b,C implies a,b are_convertible_wrt R ) by A1, Def7; :: thesis: verum