let seq be ExtREAL_sequence; :: thesis:
let p be ExtReal; :: thesis:
assume that
A1: seq is convergent and
A2: for k being Nat holds p <= seq . k ; :: thesis:
for y being ExtReal st y in rng seq holds
p <= y

let y be ExtReal; :: thesis:
assume y in rng seq ; :: thesis:
then consider x being object such that
A3: x in dom seq and
A4: y = seq . x by FUNCT_1:def 3;
reconsider x = x as Nat by A3;
seq . x >= p by A2;
hence p <= y by A4; :: thesis:

end;

then A5: p is LowerBound of rng seq by XXREAL_2:def 2;
reconsider INFSEQ = inferior_realsequence seq as sequence of ExtREAL ;
consider Y being non empty Subset of ExtREAL such that
A6: Y = { (seq . k) where k is Nat : 0 <= k } and
A7: INFSEQ . 0 = inf Y by RINFSUP2:def 6;

let x be object ; :: thesis:
assume x in rng seq ; :: thesis:
then consider k being object such that
A8: k in dom seq and
A9: x = seq . k by FUNCT_1:def 3;
thus x in Y by A6, A8, A9; :: thesis:

end;

then A10: rng seq c= Y ;
for n being Element of NAT holds sup INFSEQ >= INFSEQ . n

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

end;

then A11: sup INFSEQ >= INFSEQ . 0 ;

let x be object ; :: thesis:
assume x in Y ; :: thesis:
then consider k being Nat such that
A12: ( x = seq . k & 0 <= k ) by A6;
A13: k in NAT by ORDINAL1:def 12;
dom seq = NAT by FUNCT_2:def 1;
hence x in rng seq by A12, FUNCT_1:3, A13; :: thesis:

end;

then Y c= rng seq ;
then Y = rng seq by A10, XBOOLE_0:def 10;
then (inferior_realsequence seq) . 0 >= p by A5, A7, XXREAL_2:def 4;
then lim_inf seq >= p by A11, XXREAL_0:2;
hence p <= lim seq by A1, RINFSUP2:41; :: thesis: