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

for B being limit_ordinal infinite Ordinal st B in A & sup (SUCC /\ B) = B holds

B in SUCC

for B2 being Ordinal st B2 in A holds

ex C being Ordinal st

( C in SUCC & B2 c= C )

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

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

then reconsider SUCC = { (succ B2) where B2 is Element of A : ( B2 in X & B1 in succ B2 ) } as Subset of A ;
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;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

for B being limit_ordinal infinite Ordinal st B in A & sup (SUCC /\ B) = B holds

B in SUCC

proof

then A16:
SUCC is_closed_in A
;
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

end;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

hence
( not sup (SUCC /\ B) = B or B in SUCC )
; :: thesis: verum
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

B3 in B by A5, XBOOLE_0:def 4;

hence contradiction by A3, A15, A6, ORDINAL1:10; :: thesis: verum

end;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

then A15:
B0 in { B10 where B10 is Element of A : ( B10 is infinite & B10 is limit_ordinal & sup (X /\ B10) = B10 ) }
;
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 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

B3 in B by A5, XBOOLE_0:def 4;

hence contradiction by A3, A15, A6, ORDINAL1:10; :: thesis: verum

for B2 being Ordinal st B2 in A holds

ex C being Ordinal st

( C in SUCC & B2 c= C )

proof

then
SUCC is unbounded
by Th6;
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;( 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

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