defpred S1[ Ordinal] means On X c= $1;
for x being object st x in On X holds
x is Ordinal by ORDINAL1:def 9;
then reconsider A = union (On X) as epsilon-transitive epsilon-connected set by ORDINAL1:23;
On X c= succ A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in On X or x in succ A )
assume A1: x in On X ; :: thesis: x in succ A
then reconsider B = x as Ordinal by ORDINAL1:def 9;
B c= A by A1, ZFMISC_1:74;
hence x in succ A by ORDINAL1:22; :: thesis: verum
end;
then A2: ex A being Ordinal st S1[A] ;
thus ex F being Ordinal st
( S1[F] & ( for A being Ordinal st S1[A] holds
F c= A ) ) from ORDINAL1:sch 1(A2); :: thesis: verum