for X being ARS st X is COMP holds
for x, y being Element of X st x <=*=> y holds
nf x = nf y by Lem27;