:: deftheorem Def17 defines nf ABSRED_0:def 19 :
for X being ARS
for x being Element of X st ex y being Element of X st y is_normform_of x & ( for y, z being Element of X st y is_normform_of x & z is_normform_of x holds
y = z ) holds
for b₃ being Element of X holds
( b₃ = nf x iff b₃ is_normform_of x );