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