let seq be ExtREAL_sequence; :: thesis: superior_realsequence seq is non-increasing

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

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

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

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

consider Y being non empty Subset of ExtREAL such that

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

A2: (superior_realsequence seq) . m = sup Y by Def7;

consider Z being non empty Subset of ExtREAL such that

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

A4: (superior_realsequence seq) . n = sup Z by Def7;

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

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: (superior_realsequence seq) . m = sup Y by Def7;

consider Z being non empty Subset of ExtREAL such that

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

A4: (superior_realsequence seq) . n = sup Z by Def7;

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

Z c= Y

proof

hence
(superior_realsequence seq) . n <= (superior_realsequence seq) . m
by A2, A4, XXREAL_2:59; :: 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