let seq be ExtREAL_sequence; :: thesis: for a being R_eal st ( for n being Nat holds seq . n >= a ) holds
inf seq >= a
let a be R_eal; :: thesis: ( ( for n being Nat holds seq . n >= a ) implies inf seq >= a )
assume A1: for n being Nat holds seq . n >= a ; :: thesis: inf seq >= a

now

let x be ext-real number ; :: thesis: ( x in rng seq implies x >= a )
assume x in rng seq ; :: thesis: x >= a
then consider z being set such that
A2: z in dom seq and
A3: x = seq . z by FUNCT_1:def 5;
thus x >= a by A1, A3, A2; :: thesis: verum

end;

then a is LowerBound of rng seq by XXREAL_2:def 2;
hence inf seq >= a by XXREAL_2:def 4; :: thesis: verum