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 :: thesis: for x being ExtReal st x in rng seq holds
x >= a

let x be ExtReal; :: thesis: ( x in rng seq implies x >= a )
assume x in rng seq ; :: thesis: x >= a
then ex z being object st
( z in dom seq & x = seq . z ) by FUNCT_1:def 3;
hence x >= a by A1; :: 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