for N being ExtNat st 0 <> N holds
0 < N ;