let seq be Real_Sequence; :: thesis: ( seq is decreasing iff for n, m being Nat st n < m holds
seq . m < seq . n )
thus ( seq is decreasing implies for n, m being Nat st n < m holds
seq . m < seq . n ) :: thesis: ( ( for n, m being Nat st n < m holds
seq . m < seq . n ) implies seq is decreasing )

proof

assume seq is decreasing ; :: thesis: for n, m being Nat st n < m holds
seq . m < seq . n
then for n, k being Nat holds seq . ((n + 1) + k) < seq . n by Th3;
hence for n, m being Nat st n < m holds
seq . m < seq . n by Lm3; :: thesis: verum

end;

assume A1: for n, m being Nat st n < m holds
seq . m < seq . n ; :: thesis: seq is decreasing
let n be Nat; :: according to SEQM_3:def 2 :: thesis: for n being Nat st n in dom seq & n in dom seq & n < n holds
seq . n > seq . n
let m be Nat; :: thesis: ( n in dom seq & m in dom seq & n < m implies seq . n > seq . m )
assume that
n in dom seq and
m in dom seq and
A2: n < m ; :: thesis: seq . n > seq . m
thus seq . n > seq . m by A1, A2; :: thesis: verum