the natural-valued Function of O,F_Real is INT -valued ;
hence ex b₁ being Function of O,F_Real st b₁ is INT -valued ; :: thesis: verum