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 b,R is_a_normal_form_of b,R by Th55;
then A2: nf b,R is_a_normal_form_wrt R by Def6;
R reduces b, nf b,R by A1, Def6;
then A3: b, nf b,R are_convertible_wrt R by Th26;
A4: nf a,R is_a_normal_form_of a,R by Th55;
then R reduces a, nf a,R by Def6;
then A5: nf a,R,a 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 A5, Th31;
then A6: nf a,R, nf b,R are_convertible_wrt R by A3, Th31;
nf a,R is_a_normal_form_wrt R by A4, Def6;
hence nf a,R = nf b,R by A2, A6, Def19; :: thesis: verum