:: deftheorem Def12 defines nf REWRITE1:def 12 :
for R being Relation
for a being object st a has_a_normal_form_wrt R & ( 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 ) holds
for b₃ being set holds
( b₃ = nf (a,R) iff b₃ is_a_normal_form_of a,R );