We show (1) For each strongly normalizable lambda term M, with beta eta normal form N, there exists an intersection type A such that in BCD (without top element) we have |-M:A and N is the unique beta-eta normal term s.t.|- N:A. A similar result holds for finite sets of strongly normalizable terms. (2) For each intersection type A, if the set of all closed terms M such that in BCD (without top element) |-M:A is infinite, then when closed under beta-eta conversion this set forms an adequate numeral system for untyped lambda calculus.In particular, all these terms are generated from a single 0 by the application of a successor S, S(...(S0)...) and by beta-eta conversion.