set x = the Element of X;
1_1 ( the Element of X,F_Real) is INT -valued ;
hence ex b₁ being Series of X,F_Real st b₁ is INT -valued ; :: thesis: verum