let M be non countable Aleph; :: thesis: for X being Subset of M st omega in cf M & X is unbounded holds

limpoints X is unbounded

let X be Subset of M; :: thesis: ( omega in cf M & X is unbounded implies limpoints X is unbounded )

assume A1: omega in cf M ; :: thesis: ( not X is unbounded or limpoints X is unbounded )

assume A2: X is unbounded ; :: thesis: limpoints X is unbounded

for B1 being Ordinal st B1 in M holds

ex C being Ordinal st

( C in limpoints X & B1 c= C )

limpoints X is unbounded

let X be Subset of M; :: thesis: ( omega in cf M & X is unbounded implies limpoints X is unbounded )

assume A1: omega in cf M ; :: thesis: ( not X is unbounded or limpoints X is unbounded )

assume A2: X is unbounded ; :: thesis: limpoints X is unbounded

for B1 being Ordinal st B1 in M holds

ex C being Ordinal st

( C in limpoints X & B1 c= C )

proof

hence
limpoints X is unbounded
by Th6; :: thesis: verum
let B1 be Ordinal; :: thesis: ( B1 in M implies ex C being Ordinal st

( C in limpoints X & B1 c= C ) )

assume B1 in M ; :: thesis: ex C being Ordinal st

( C in limpoints X & B1 c= C )

then consider B being limit_ordinal infinite Ordinal such that

B in M and

A3: ( B1 in B & B in limpoints X ) by A1, A2, Th24;

take B ; :: thesis: ( B in limpoints X & B1 c= B )

thus ( B in limpoints X & B1 c= B ) by A3, ORDINAL1:def 2; :: thesis: verum

end;( C in limpoints X & B1 c= C ) )

assume B1 in M ; :: thesis: ex C being Ordinal st

( C in limpoints X & B1 c= C )

then consider B being limit_ordinal infinite Ordinal such that

B in M and

A3: ( B1 in B & B in limpoints X ) by A1, A2, Th24;

take B ; :: thesis: ( B in limpoints X & B1 c= B )

thus ( B in limpoints X & B1 c= B ) by A3, ORDINAL1:def 2; :: thesis: verum