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

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 = {} )
;

end;

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

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;then sup (rng f) = {} by ORDINAL2:18, RELAT_1:38;

hence sup (rng f) in M by ORDINAL1:16, XBOOLE_1:3; :: thesis: verum