for X being 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