:: deftheorem defines N.F. ABSRED_0:def 18 :
for X being ARS holds
( X is N.F. iff for x, y being Element of X st x is normform & x <=*=> y holds
y =*=> x );