let R be weakly-normalizing with_UN_property Relation; :: thesis: for a being set holds nf a,R is_a_normal_form_of a,R
let a be set ; :: thesis: nf a,R is_a_normal_form_of a,R
( a in field R or not a in field R ) ;
then A1: a has_a_normal_form_wrt R by Def14, Th47;
for b, c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c by Th54;
hence nf a,R is_a_normal_form_of a,R by A1, Def12; :: thesis: verum