let seq be ExtREAL_sequence; :: thesis: for a being R_eal st ( for n being Nat holds seq . n <= a ) holds
sup seq <= a
let a be R_eal; :: thesis: ( ( for n being Nat holds seq . n <= a ) implies sup seq <= a )
assume A1: for n being Nat holds seq . n <= a ; :: thesis: sup 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 UpperBound of rng seq by XXREAL_2:def 1;
hence sup seq <= a by XXREAL_2:def 3; :: thesis: verum