[TYPES] Question about the polymorphic lambda calculus

[Samuel E. Moelius III]

Suppose that T is a type with exactly one free variable X.  Further
suppose that for every closed type U, there is some term with type
T[U/X].  Then, does there necessarily exist some term with type (forall
X. T)?

In other words, in the situation described above, can the meta-level 
``forall'' be pushed down into the types?

If this is a theorem, could someone please point me to a proof of it?

Thanks in advance.

Sam Moelius