let x be number ; :: thesis: ( x is real & x is ext-integer implies x is integer )
assume ( x in REAL & ( x is integer or x = +infty ) ) ; :: according to XREAL_0:def 1,FVALUAT1:def 1 :: thesis: x is integer
hence x is integer ; :: thesis: verum