:: deftheorem defines UN* ABSRED_0:def 16 :
for X being ARS holds
( X is UN* iff for x, y, z being Element of X st y is_normform_of x & z is_normform_of x holds
y = z );