let seq be ExtREAL_sequence; :: thesis: for r being R_eal st ( for n being Nat holds r <= seq . n ) holds
r <= lim_inf seq
let r be R_eal; :: thesis: ( ( for n being Nat holds r <= seq . n ) implies r <= lim_inf seq )
assume A1: for n being Nat holds r <= seq . n ; :: thesis: r <= lim_inf seq
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 f . n <= seq . n

proof

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

end;

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