let x be object ; :: thesis: ( x is natural implies x is ext-natural )
assume x is natural ; :: thesis: x is ext-natural
then x in NAT by ORDINAL1:def 12;
hence x is ext-natural by Th1, XBOOLE_0:def 8, TARSKI:def 3; :: thesis: verum