let M be non countable Aleph; :: thesis: for X being Subset of M st omega in cf M holds
for f being sequence of X holds sup (rng f) in M
let X be Subset of M; :: thesis: ( omega in cf M implies for f being sequence of X holds sup (rng f) in M )
assume A1: omega in cf M ; :: thesis: for f being sequence of X holds sup (rng f) in M
let f be sequence of X; :: thesis: sup (rng f) in M
per cases ( not X = {} or X = {} ) ;
suppose A2: not X = {} ; :: thesis: sup (rng f) in M
rng f c= X by RELAT_1:def 19;
then A3: rng f c= M by XBOOLE_1:1;
A4: card NAT in cf M by A1;
dom f = NAT by A2, FUNCT_2:def 1;
then card (rng f) c= card NAT by CARD_1:12;
then card (rng f) in cf M by A4, ORDINAL1:12;
hence sup (rng f) in M by A3, CARD_5:26; :: thesis: verum
end;
suppose X = {} ; :: thesis: sup (rng f) in M
then f = {} ;
then sup (rng f) = {} by ORDINAL2:18, RELAT_1:38;
hence sup (rng f) in M by ORDINAL1:16, XBOOLE_1:3; :: thesis: verum
end;
end;