for x being set
for R being weakly-normalizing with_UN_property Relation holds nf ((nf (x,R)),R) = nf (x,R)