:: deftheorem defines WN ABSRED_0:def 14 :
for X being ARS holds
( X is WN iff for x being Element of X holds x is normalizable );