let X be non empty set ; for R being Relation of X st R is with_UN_property & R is weakly-normalizing holds
for x being Element of X holds nf (x,R) in X
let R be Relation of X; ( R is with_UN_property & R is weakly-normalizing implies for x being Element of X holds nf (x,R) in X )
assume A1:
( R is with_UN_property & R is weakly-normalizing )
; for x being Element of X holds nf (x,R) in X
let x be Element of X; nf (x,R) in X
nf (x,R) is_a_normal_form_of x,R
by A1, REWRITE1:54;
then
R reduces x, nf (x,R)
;
hence
nf (x,R) in X
by Th74; verum