let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A st X is unbounded & limpoints X is bounded holds
ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )
let X be Subset of A; :: thesis: ( X is unbounded & limpoints X is bounded implies ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A ) )
assume A1: X is unbounded ; :: thesis: ( not limpoints X is bounded or ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A ) )
assume limpoints X is bounded ; :: thesis: ex B1 being Ordinal st
( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )
then consider B1 being Ordinal such that
A2: B1 in A and
A3: limpoints X c= B1 by Th4;
take B1 ; :: thesis: ( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A )
set SUCC = { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } ;
{ (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } c= A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } or x in A )
assume x in { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } ; :: thesis: x in A
then ex B2 being Element of A st
( x = succ B2 & B2 in X & B1 in succ B2 ) ;
hence x in A by ORDINAL1:28; :: thesis: verum

end;

then reconsider SUCC = { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } as Subset of A ;
for B being limit_ordinal infinite Ordinal st B in A & sup (SUCC /\ B) = B holds
B in SUCC

proof

let B be limit_ordinal infinite Ordinal; :: thesis: ( B in A & sup (SUCC /\ B) = B implies B in SUCC )
assume B in A ; :: thesis: ( not sup (SUCC /\ B) = B or B in SUCC )
then reconsider B0 = B as Element of A ;
not sup (SUCC /\ B) = B

proof

set B2 = the Element of B;
assume A4: sup (SUCC /\ B) = B ; :: thesis: contradiction
then consider B3 being Ordinal such that
A5: B3 in SUCC /\ B and
the Element of B c= B3 by ORDINAL2:21;
B3 in SUCC by A5, XBOOLE_0:def 4;
then A6: ex B4 being Element of A st
( B3 = succ B4 & B4 in X & B1 in succ B4 ) ;
sup (X /\ B) = B

proof

assume not sup (X /\ B) = B ; :: thesis: contradiction
then consider B5 being Ordinal such that
A7: B5 in B and
A8: X /\ B c= B5 by Th5;
succ B5 in B by A7, ORDINAL1:28;
then succ (succ B5) in B by ORDINAL1:28;
then consider B6 being Ordinal such that
A9: B6 in SUCC /\ B and
A10: succ (succ B5) c= B6 by A4, ORDINAL2:21;
A11: B6 in B by A9, XBOOLE_0:def 4;
B6 in SUCC by A9, XBOOLE_0:def 4;
then consider B7 being Element of A such that
A12: B6 = succ B7 and
A13: B7 in X and
B1 in succ B7 ;
B7 in succ B7 by ORDINAL1:6;
then B7 in B by A12, A11, ORDINAL1:10;
then B7 in X /\ B by A13, XBOOLE_0:def 4;
then A14: B7 in B5 by A8;
succ B5 in succ B7 by A10, A12, ORDINAL1:21;
then succ B5 c= B7 by ORDINAL1:22;
hence contradiction by A14, ORDINAL1:21; :: thesis: verum

end;

then A15: B0 in { B10 where B10 is Element of A : ( B10 is infinite & B10 is limit_ordinal & sup (X /\ B10) = B10 ) } ;
B3 in B by A5, XBOOLE_0:def 4;
hence contradiction by A3, A15, A6, ORDINAL1:10; :: thesis: verum

end;

hence ( not sup (SUCC /\ B) = B or B in SUCC ) ; :: thesis: verum

end;

then A16: SUCC is_closed_in A ;
for B2 being Ordinal st B2 in A holds
ex C being Ordinal st
( C in SUCC & B2 c= C )

proof

let B2 be Ordinal; :: thesis: ( B2 in A implies ex C being Ordinal st
( C in SUCC & B2 c= C ) )
assume A17: B2 in A ; :: thesis: ex C being Ordinal st
( C in SUCC & B2 c= C )
set B21 = B2 \/ B1;
B2 \/ B1 in A by A2, A17, ORDINAL3:12;
then consider D being Ordinal such that
A18: D in X and
A19: B2 \/ B1 c= D by A1, Th6;
take succ D ; :: thesis: ( succ D in SUCC & B2 c= succ D )
B2 \/ B1 in succ D by A19, ORDINAL1:22;
then B1 in succ D by ORDINAL1:12, XBOOLE_1:7;
hence succ D in SUCC by A18; :: thesis: B2 c= succ D
B2 c= B2 \/ B1 by XBOOLE_1:7;
then B2 c= D by A19;
then B2 in succ D by ORDINAL1:22;
hence B2 c= succ D by ORDINAL1:def 2; :: thesis: verum

end;

then SUCC is unbounded by Th6;
then sup SUCC = A ;
then SUCC is_unbounded_in A ;
hence ( B1 in A & { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } is_club_in A ) by A2, A16; :: thesis: verum