theorem LemN7: :: ABSRED_0:108

for X being ARS
for x, y, z being Element of X st x is_normform_of y & z =*=> y holds
x is_normform_of z by Th3;