let x be set ; :: thesis: for R being weakly-normalizing with_UN_property Relation st x is_a_normal_form_wrt R holds
nf (x,R) = x
let R be weakly-normalizing with_UN_property Relation; :: thesis: ( x is_a_normal_form_wrt R implies nf (x,R) = x )
assume A1: x is_a_normal_form_wrt R ; :: thesis: nf (x,R) = x
A2: x is_a_normal_form_of x,R by A1, REWRITE1:12;
then A3: x has_a_normal_form_wrt R ;
for b, c being object st b is_a_normal_form_of x,R & c is_a_normal_form_of x,R holds
b = c by REWRITE1:53;
hence nf (x,R) = x by A2, A3, REWRITE1:def 12; :: thesis: verum