let seq be ExtREAL_sequence; :: thesis: inferior_realsequence seq is non-decreasing

now :: thesis: for n, m being Nat st m <= n holds

(inferior_realsequence seq) . m <= (inferior_realsequence seq) . n

hence
inferior_realsequence seq is non-decreasing
; :: thesis: verum(inferior_realsequence seq) . m <= (inferior_realsequence seq) . n

let n, m be Nat; :: thesis: ( m <= n implies (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n )

consider Y being non empty Subset of ExtREAL such that

A1: Y = { (seq . k) where k is Nat : m <= k } and

A2: (inferior_realsequence seq) . m = inf Y by Def6;

consider Z being non empty Subset of ExtREAL such that

A3: Z = { (seq . k) where k is Nat : n <= k } and

A4: (inferior_realsequence seq) . n = inf Z by Def6;

assume A5: m <= n ; :: thesis: (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n

Z c= Y

end;consider Y being non empty Subset of ExtREAL such that

A1: Y = { (seq . k) where k is Nat : m <= k } and

A2: (inferior_realsequence seq) . m = inf Y by Def6;

consider Z being non empty Subset of ExtREAL such that

A3: Z = { (seq . k) where k is Nat : n <= k } and

A4: (inferior_realsequence seq) . n = inf Z by Def6;

assume A5: m <= n ; :: thesis: (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n

Z c= Y

proof

hence
(inferior_realsequence seq) . m <= (inferior_realsequence seq) . n
by A2, A4, XXREAL_2:60; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Z or z in Y )

assume z in Z ; :: thesis: z in Y

then consider k being Nat such that

A6: z = seq . k and

A7: n <= k by A3;

m <= k by A5, A7, XXREAL_0:2;

hence z in Y by A1, A6; :: thesis: verum

end;assume z in Z ; :: thesis: z in Y

then consider k being Nat such that

A6: z = seq . k and

A7: n <= k by A3;

m <= k by A5, A7, XXREAL_0:2;

hence z in Y by A1, A6; :: thesis: verum