let a be finite Ordinal; :: thesis: for x being set holds
( not x in a or x = 0 or ex b being ordinal number st x = succ b )
let x be set ; :: thesis: ( not x in a or x = 0 or ex b being ordinal number st x = succ b )
assume Z0: ( x in a & x <> 0 ) ; :: thesis: ex b being ordinal number st x = succ b
then A1: {} in x by ORDINAL3:8;

now

assume x is limit_ordinal ; :: thesis: contradiction
then ( omega c= x & x c= a ) by Z0, A1, ORDINAL1:def 2, ORDINAL1:def 11;
hence contradiction ; :: thesis: verum

end;

hence ex b being ordinal number st x = succ b by Z0, ORDINAL1:29; :: thesis: verum