let a be number ; :: thesis: ( a is natural implies a is ext-real )
assume a is natural ; :: thesis: a is ext-real
then a in NAT by ORDINAL1:def 12;
hence a in ExtREAL by XBOOLE_0:def 3; :: according to XXREAL_0:def 1 :: thesis: verum