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