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

( (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