let X be non empty set ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: for x being Element of X holds nf (x,R) in X
let x be Element of X; :: thesis: 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; :: thesis: verum