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