for X being ARS
for x, y being Element of X st x is normform & y ==> x holds
x is_normform_of y by Th2;