let n be Element of 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: seq . n in rng seq by FUNCT_2:6;
( inf (rng seq) is LowerBound of rng seq & sup (rng seq) is UpperBound of rng seq ) by XXREAL_2:def 3, XXREAL_2:def 4;
hence ( inf seq <= seq . n & seq . n <= sup seq ) by A1, XXREAL_2:def 1, XXREAL_2:def 2; :: thesis: verum