let x be set ; :: thesis: ( x is finite & x is ext-natural implies x is natural )
assume ( x is finite & x is ext-natural ) ; :: thesis: x is natural
then ( x in ExtNAT & not x in {+infty} ) by XXREAL_0:def 2, TARSKI:def 1;
then x in NAT by XBOOLE_0:def 3;
hence x is natural ; :: thesis: verum