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

now

let n, m be Element of NAT ; :: thesis: ( m <= n implies (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n )
assume A1: m <= n ; :: thesis: (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n
consider Y being non empty Subset of ExtREAL such that
A2: ( Y = { (seq . k) where k is Element of NAT : m <= k } & (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 Element of NAT : n <= k } & (inferior_realsequence seq) . n = inf Z ) by Def6;
Z c= Y

proof

let z be set ; :: 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 Element of NAT such that
A4: ( z = seq . k & n <= k ) by A3;
m <= k by A1, A4, XXREAL_0:2;
hence z in Y by A2, A4; :: thesis: verum

end;

hence (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n by A2, A3, XXREAL_2:60; :: thesis: verum

end;

hence inferior_realsequence seq is non-decreasing by Th7; :: thesis: verum