for n being Nat holds
( n = {} or ex m being Nat st n = succ m )