let x be set ; :: thesis: ( x is Ordinal implies succ x is Ordinal )
assume A1: x is Ordinal ; :: thesis: succ x is Ordinal

A2: now

let y be set ; :: thesis: ( not y in succ x or y in x or y = x )
assume A3: y in succ x ; :: thesis: ( y in x or y = x )
( y in {x} implies y = x ) by TARSKI:def 1;
hence ( y in x or y = x ) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in succ x implies y c= succ x )
assume A4: y in succ x ; :: thesis: y c= succ x

A5: now

assume y in x ; :: thesis: y c= succ x
then A6: y c= x by A1, Def2;
x c= x \/ {x} by XBOOLE_1:7;
hence y c= succ x by A6, XBOOLE_1:1; :: thesis: verum

end;

( y = x implies y c= succ x ) by XBOOLE_1:7;
hence y c= succ x by A2, A4, A5; :: thesis: verum

end;

then A7: succ x is epsilon-transitive by Def2;

now

let y, z be set ; :: thesis: ( y in succ x & z in succ x & not y in z & not y = z implies z in y )
assume A8: ( y in succ x & z in succ x ) ; :: thesis: ( y in z or y = z or z in y )
then A9: ( y in x or y = x ) by A2;
( z in x or z = x ) by A2, A8;
hence ( y in z or y = z or z in y ) by A1, A9, Def3; :: thesis: verum

end;

then succ x is epsilon-connected by Def3;
hence succ x is Ordinal by A7; :: thesis: verum