let x be Element of X; :: thesis: ( x is normform implies x is normalizable )
assume A1: x is normform ; :: thesis: x is normalizable
take x ; :: according to ABSRED_0:def 13 :: thesis: x is_normform_of x
thus x is_normform_of x by A1; :: thesis: verum