let D be Ordinal; :: thesis: ex A being Ordinal st
( D in A & A is limit_ordinal )
consider Field being set such that
A1: D in Field and
A2: for X, Y being set st X in Field & Y c= X holds
Y in Field and
A3: for X being set st X in Field holds
bool X in Field and
for X being set holds
( not X c= Field or X,Field are_equipotent or X in Field ) by ZFMISC_1:112;
for X being set st X in On Field holds
( X is Ordinal & X c= On Field )

proof

let X be set ; :: thesis: ( X in On Field implies ( X is Ordinal & X c= On Field ) )
assume A4: X in On Field ; :: thesis: ( X is Ordinal & X c= On Field )
then reconsider A = X as Ordinal by Def9;
A5: A in Field by A4, Def9;
thus X is Ordinal by A4, Def9; :: thesis: X c= On Field
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in On Field )
assume A6: y in X ; :: thesis: y in On Field
then y in A ;
then reconsider B = y as Ordinal by Th9;
B c= A by A6, Def2;
then B in Field by A2, A5;
hence y in On Field by Def9; :: thesis: verum

end;

then reconsider ON = On Field as epsilon-transitive epsilon-connected set by Th15;
take ON ; :: thesis: ( D in ON & ON is limit_ordinal )
thus D in ON by A1, Def9; :: thesis: ON is limit_ordinal
for A being Ordinal st A in ON holds
succ A in ON

proof

let A be Ordinal; :: thesis: ( A in ON implies succ A in ON )
A7: succ A c= bool A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in succ A or x in bool A )
reconsider xx = x as set by TARSKI:1;
assume x in succ A ; :: thesis: x in bool A
then ( x in A or x = A ) by Th4;
then xx c= A by Def2;
hence x in bool A ; :: thesis: verum

end;

assume A in ON ; :: thesis: succ A in ON
then A in Field by Def9;
then bool A in Field by A3;
then succ A in Field by A2, A7;
hence succ A in ON by Def9; :: thesis: verum

end;

hence ON is limit_ordinal by Th24; :: thesis: verum