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
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
proof
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;
hence (superior_realsequence seq) . n <= (superior_realsequence seq) . m by A2, A4, XXREAL_2:59; :: thesis: verum
end;
hence superior_realsequence seq is non-increasing ; :: thesis: verum