theorem LmA: :: ABSRED_0:113

for X being ARS
for x, y being Element of X st x <> y & ( for a, b being Element of X holds
( a ==> b iff a = x ) ) holds
( y is normform & x is normalizable )