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 & ( for X, Y being set st X in Field & Y c= X holds
Y in Field ) & ( for X being set st X in Field holds
bool X in Field ) & ( for X being set holds
( not X c= Field or X,Field are_equipotent or X in Field ) ) ) by ZFMISC_1:136;
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 A2: X in On Field ; :: thesis: ( X is Ordinal & X c= On Field )
hence X is Ordinal by Def10; :: thesis: X c= On Field
reconsider A = X as Ordinal by A2, Def10;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in On Field )
assume A3: y in X ; :: thesis: y in On Field
then y in A ;
then reconsider B = y as Ordinal by Th23;
( B c= A & A in Field ) by A2, A3, Def2, Def10;
then B in Field by A1;
hence y in On Field by Def10; :: thesis: verum

end;

then reconsider ON = On Field as Ordinal by Th31;
take ON ; :: thesis: ( D in ON & ON is limit_ordinal )
thus D in ON by A1, Def10; :: 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 )
assume A in ON ; :: thesis: succ A in ON
then A in Field by Def10;
then A4: bool A in Field by A1;
succ A c= bool A

proof

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

end;

then succ A in Field by A1, A4;
hence succ A in ON by Def10; :: thesis: verum

end;

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