let D be Ordinal; :: thesis:
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 )

let X be set ; :: thesis:
assume A4: X in On Field ; :: thesis:
then reconsider A = X as Ordinal by Def9;
A5: A in Field by A4, Def9;
thus X is Ordinal by A4, Def9; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: y in X ; :: thesis:
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:

end;

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

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

end;

assume A in ON ; :: thesis:
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:

end;