let a be finite Ordinal; :: thesis: for x being set holds
( not x in a or x = 0 or ex b being Ordinal st x = succ b )
let x be set ; :: thesis: ( not x in a or x = 0 or ex b being Ordinal st x = succ b )
assume A1: ( x in a & x <> 0 ) ; :: thesis: ex b being Ordinal st x = succ b
then A2: {} in x by ORDINAL3:8;
now :: thesis: not x is limit_ordinal
assume x is limit_ordinal ; :: thesis: contradiction
then ( omega c= x & x c= a ) by A1, A2, ORDINAL1:def 2, ORDINAL1:def 11;
hence contradiction ; :: thesis: verum
end;
hence ex b being Ordinal st x = succ b by A1, ORDINAL1:29; :: thesis: verum