let seq be ExtREAL_sequence; :: thesis: for p being ext-real number st seq is convergent & ( for k being Nat holds p <= seq . k ) holds
p <= lim seq
let p be ext-real number ; :: thesis: ( seq is convergent & ( for k being Nat holds p <= seq . k ) implies p <= lim seq )
assume that
A1: seq is convergent and
A2: for k being Nat holds p <= seq . k ; :: thesis: p <= lim seq
for y being ext-real number st y in rng seq holds
p <= y

proof

let y be ext-real number ; :: thesis: ( y in rng seq implies p <= y )
assume y in rng seq ; :: thesis: p <= y
then consider x being set such that
A4: ( x in dom seq & y = seq . x ) by FUNCT_1:def 5;
reconsider x = x as Nat by A4;
seq . x >= p by A2;
hence p <= y by A4; :: thesis: verum

end;

then B1: p is LowerBound of rng seq by XXREAL_2:def 2;
reconsider INFSEQ = inferior_realsequence seq as Function of NAT ,ExtREAL ;
for n being Element of NAT holds sup INFSEQ >= INFSEQ . n

proof

let n be Element of NAT ; :: thesis: sup INFSEQ >= INFSEQ . n
NAT = dom INFSEQ by FUNCT_2:def 1;
then INFSEQ . n in rng INFSEQ by FUNCT_1:def 5;
hence sup INFSEQ >= INFSEQ . n by XXREAL_2:4; :: thesis: verum

end;

then B2: sup INFSEQ >= INFSEQ . 0 ;
consider Y being non empty Subset of ExtREAL such that
A9: ( Y = { (seq . k) where k is Element of NAT : 0 <= k } & INFSEQ . 0 = inf Y ) by RINFSUP2:def 6;

now

let x be set ; :: thesis: ( x in Y implies x in rng seq )
assume x in Y ; :: thesis: x in rng seq
then C1: ex k being Element of NAT st
( x = seq . k & 0 <= k ) by A9;
dom seq = NAT by FUNCT_2:def 1;
hence x in rng seq by C1, FUNCT_1:12; :: thesis: verum

end;

then C2: Y c= rng seq by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in rng seq implies x in Y )
assume x in rng seq ; :: thesis: x in Y
then consider k being set such that
C3: ( k in dom seq & x = seq . k ) by FUNCT_1:def 5;
reconsider k = k as Element of NAT by C3;
thus x in Y by A9, C3; :: thesis: verum

end;

then rng seq c= Y by TARSKI:def 3;
then Y = rng seq by C2, XBOOLE_0:def 10;
then (inferior_realsequence seq) . 0 >= p by B1, A9, XXREAL_2:def 4;
then lim_inf seq >= p by B2, XXREAL_0:2;
hence p <= lim seq by A1, RINFSUP2:41; :: thesis: verum