for x being object holds
( x is ExtNat iff ( x is Nat or x = +infty ) )