let A be Ordinal; :: thesis: ( A is limit_ordinal iff for C being Ordinal st C in A holds
succ C in A )
thus ( A is limit_ordinal implies for C being Ordinal st C in A holds
succ C in A ) :: thesis: ( ( for C being Ordinal st C in A holds
succ C in A ) implies A is limit_ordinal )

proof

assume A is limit_ordinal ; :: thesis: for C being Ordinal st C in A holds
succ C in A
then A1: A = union A by Def6;
let C be Ordinal; :: thesis: ( C in A implies succ C in A )
assume C in A ; :: thesis: succ C in A
then consider z being set such that
A2: ( C in z & z in A ) by A1, TARSKI:def 4;
for b being set st b in {C} holds
b in z by A2, TARSKI:def 1;
then A3: {C} c= z by TARSKI:def 3;
A4: z is Ordinal by A2, Th23;
then C c= z by A2, Def2;
then succ C c= z by A3, XBOOLE_1:8;
then ( succ C = z or succ C c< z ) by XBOOLE_0:def 8;
then A5: ( succ C = z or succ C in z ) by A4, Th21;
z c= A by A2, Def2;
hence succ C in A by A2, A5; :: thesis: verum

end;

assume A6: for C being Ordinal st C in A holds
succ C in A ; :: thesis: A is limit_ordinal

now

let a be set ; :: thesis: ( a in A implies a in union A )
assume A7: a in A ; :: thesis: a in union A
then a is Ordinal by Th23;
then A8: succ a in A by A6, A7;
a in succ a by Th10;
hence a in union A by A8, TARSKI:def 4; :: thesis: verum

end;

then A9: A c= union A by TARSKI:def 3;

now

let a be set ; :: thesis: ( a in union A implies a in A )
assume a in union A ; :: thesis: a in A
then consider z being set such that
A10: ( a in z & z in A ) by TARSKI:def 4;
z c= A by A10, Def2;
hence a in A by A10; :: thesis: verum

end;

then union A c= A by TARSKI:def 3;
then A = union A by A9, XBOOLE_0:def 10;
hence A is limit_ordinal by Def6; :: thesis: verum