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:55;
then R reduces x, nf x,R by REWRITE1:def 6;
hence nf x,R in X by Th75; :: thesis: verum