let n be Nat; :: thesis: for seq being ExtREAL_sequence holds
( inf seq <= seq . n & seq . n <= sup seq )
let seq be ExtREAL_sequence; :: thesis: ( inf seq <= seq . n & seq . n <= sup seq )
A1: inf (rng seq) is LowerBound of rng seq by XXREAL_2:def 4;
A2: sup (rng seq) is UpperBound of rng seq by XXREAL_2:def 3;
n in NAT by ORDINAL1:def 12;
then seq . n in rng seq by FUNCT_2:4;
hence ( inf seq <= seq . n & seq . n <= sup seq ) by A1, A2, XXREAL_2:def 1, XXREAL_2:def 2; :: thesis: verum