for a being finite Ordinal
for x being set holds
( not x in a or x = 0 or ex b being Ordinal st x = succ b )