let R be weakly-normalizing with_UN_property Relation; :: thesis: for a being object holds nf (a,R) is_a_normal_form_of a,R
let a be object ; :: 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, Th46;
for b, c being object st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R holds
b = c by Th53;
hence nf (a,R) is_a_normal_form_of a,R by A1, Def12; :: thesis: verum