let x be number ; :: thesis: ( x is natural implies x is real )
assume x is natural ; :: thesis: x is real
then x in NAT by ORDINAL1:def 13;
hence x in REAL ; :: according to XREAL_0:def 1 :: thesis: verum