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

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