let seq be ExtREAL_sequence; :: thesis: for r being R_eal st ( for n being Nat holds seq . n <= r ) holds
lim_sup seq <= r
let r be R_eal; :: thesis: ( ( for n being Nat holds seq . n <= r ) implies lim_sup seq <= r )
assume A1: for n being Nat holds seq . n <= r ; :: thesis: lim_sup seq <= r
deffunc H₁( Element of NAT ) -> R_eal = r;
consider f being Function of NAT,ExtREAL such that
A2: for n being Element of NAT holds f . n = H₁(n) from FUNCT_2:sch 4();
A4: for n being Nat holds f . n = r

proof

let n be Nat; :: thesis: f . n = r
n is Element of NAT by ORDINAL1:def 12;
hence f . n = r by A2; :: thesis: verum

end;

then A5: ( f is convergent & lim f = r ) by MESFUNC5:60;
for n being Nat holds seq . n <= f . n

proof

let n be Nat; :: thesis: seq . n <= f . n
f . n = r by A4;
hence seq . n <= f . n by A1; :: thesis: verum

end;

then lim_sup seq <= lim_sup f by MESFUN10:3;
hence lim_sup seq <= r by A5, RINFSUP2:41; :: thesis: verum