theorem Th35: :: CARD_1:36

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