theorem Th84: :: EXCHSORT:84

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 )