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 )

proof

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;

hence limpoints X is unbounded by Th6; :: thesis: verum