let x be set ; :: thesis: ( x is Ordinal implies succ x is Ordinal )
A1: now :: thesis: for y being set holds
( not y in succ x or y in x or y = x )
let y be set ; :: thesis: ( not y in succ x or y in x or y = x )
A2: ( y in {x} implies y = x ) by TARSKI:def 1;
assume y in succ x ; :: thesis: ( y in x or y = x )
hence ( y in x or y = x ) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
assume A3: x is Ordinal ; :: thesis: succ x is Ordinal
now :: thesis: for y being set st y in succ x holds
y c= succ x
let y be set ; :: thesis: ( y in succ x implies y c= succ x )
A4: ( y = x implies y c= succ x ) by XBOOLE_1:7;
A5: now :: thesis: ( y in x implies y c= succ x )
assume y in x ; :: thesis: y c= succ x
then A6: y c= x by A3, Def2;
x c= x \/ {x} by XBOOLE_1:7;
hence y c= succ x by A6; :: thesis: verum
end;
assume y in succ x ; :: thesis: y c= succ x
hence y c= succ x by A1, A5, A4; :: thesis: verum
end;
then A7: succ x is epsilon-transitive ;
now :: thesis: for y, z being set st y in succ x & z in succ x & not y in z & not y = z holds
z in y
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 that
A8: y in succ x and
A9: z in succ x ; :: thesis: ( y in z or y = z or z in y )
A10: ( z in x or z = x ) by A1, A9;
( y in x or y = x ) by A1, A8;
hence ( y in z or y = z or z in y ) by A3, A10, Def3; :: thesis: verum
end;
then succ x is epsilon-connected ;
hence succ x is Ordinal by A7; :: thesis: verum