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