theorem LemN5: :: ABSRED_0:110

for X being ARS
for x, y being Element of X st x is normalizable & y ==> x holds
y is normalizable by LemN6;