let R be weakly-normalizing with_UN_property Relation; :: thesis: for a, b being set st a,b are_convertible_wrt R holds
nf a,R = nf b,R
let a, b be set ; :: thesis: ( a,b are_convertible_wrt R implies nf a,R = nf b,R )
A1: ( nf a,R is_a_normal_form_of a,R & nf b,R is_a_normal_form_of b,R ) by Th55;
then A2: ( nf a,R is_a_normal_form_wrt R & nf b,R is_a_normal_form_wrt R ) by Def6;
( R reduces a, nf a,R & R reduces b, nf b,R ) by A1, Def6;
then A3: ( nf a,R,a are_convertible_wrt R & b, nf b,R are_convertible_wrt R ) by Th26;
assume a,b are_convertible_wrt R ; :: thesis: nf a,R = nf b,R
then nf a,R,b are_convertible_wrt R by A3, Th31;
then nf a,R, nf b,R are_convertible_wrt R by A3, Th31;
hence nf a,R = nf b,R by A2, Def19; :: thesis: verum