let N, M be ExtNat; :: thesis: ( M in NAT & N <= M implies N in NAT )
assume A1: ( M in NAT & N <= M ) ; :: thesis: N in NAT
( 0 <= N & 0 in REAL ) by XREAL_0:def 1;
then N in REAL by A1, NUMBERS:19, XXREAL_0:45;
then N is Nat by Th3;
hence N in NAT by ORDINAL1:def 12; :: thesis: verum