:: deftheorem defines is_normform_of ABSRED_0:def 12 :
for X being ARS
for x, y being Element of X holds
( x is_normform_of y iff ( x is normform & y =*=> x ) );