for R being weakly-normalizing with_UN_property Relation
for a being object holds nf (a,R) is_a_normal_form_of a,R