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