let x be object ; :: thesis: ( x is ExtNat iff ( x is Nat or x = +infty ) )

hereby :: thesis: ( ( x is Nat or x = +infty ) implies x is ExtNat )

assume x is ExtNat ; :: thesis: ( x is Nat or x = +infty )
then ( x in NAT or x = +infty ) by Def1, ZFMISC_1:136;
hence ( x is Nat or x = +infty ) ; :: thesis: verum

end;

assume ( x is Nat or x = +infty ) ; :: thesis: x is ExtNat
then ( x in NAT or x in {+infty} ) by ORDINAL1:def 12, TARSKI:def 1;
then x in ExtNAT by XBOOLE_0:def 3;
hence x is ExtNat ; :: thesis: verum