let n be Nat; :: thesis: for seq being ExtREAL_sequence holds
( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n )
let seq be ExtREAL_sequence; :: thesis: ( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n )
consider Y being non empty Subset of ExtREAL such that
A1: Y = { (seq . k) where k is Nat : n <= k } and
A2: (inferior_realsequence seq) . n = inf Y by Def6;
A3: seq . n in Y by A1;
hence (inferior_realsequence seq) . n <= seq . n by A2, XXREAL_2:3; :: thesis: seq . n <= (superior_realsequence seq) . n
ex Z being non empty Subset of ExtREAL st
( Z = { (seq . k) where k is Nat : n <= k } & (superior_realsequence seq) . n = sup Z ) by Def7;
hence seq . n <= (superior_realsequence seq) . n by A1, A3, XXREAL_2:4; :: thesis: verum