for N being ExtNat holds
( N = 0 or ex K being ExtNat st N = K + 1 )