let seq be Real_Sequence; :: thesis: ( ( ( for n being Element of NAT holds seq . (n + 1) < seq . n ) implies for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) & ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n ) )
thus ( ( for n being Element of NAT holds seq . (n + 1) < seq . n ) implies for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) :: thesis: ( ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) & ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n ) )

proof

assume A1: for n being Element of NAT holds seq . (n + 1) < seq . n ; :: thesis: for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n
let n be Element of NAT ; :: thesis: for k being Element of NAT holds seq . ((n + 1) + k) < seq . n
defpred S₁[ Element of NAT ] means seq . ((n + 1) + $1) < seq . n;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
seq . (((n + 1) + k) + 1) < seq . ((n + 1) + k) by A1;
hence S₁[k + 1] by A3, XXREAL_0:2; :: thesis: verum

end;

A4: S₁[ 0 ] by A1;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A2); :: thesis: verum

end;

thus ( ( for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ) implies for n, m being Element of NAT st n < m holds
seq . m < seq . n ) :: thesis: ( ( for n, m being Element of NAT st n < m holds
seq . m < seq . n ) implies for n being Element of NAT holds seq . (n + 1) < seq . n )

proof

assume A5: for n, k being Element of NAT holds seq . ((n + 1) + k) < seq . n ; :: thesis: for n, m being Element of NAT st n < m holds
seq . m < seq . n
let n, m be Element of NAT ; :: thesis: ( n < m implies seq . m < seq . n )
assume n < m ; :: thesis: seq . m < seq . n
then ex k being Element of NAT st m = (n + 1) + k by Lm1;
hence seq . m < seq . n by A5; :: thesis: verum

end;

assume A6: for n, m being Element of NAT st n < m holds
seq . m < seq . n ; :: thesis: for n being Element of NAT holds seq . (n + 1) < seq . n
let n be Element of NAT ; :: thesis: seq . (n + 1) < seq . n
n < n + 1 by NAT_1:13;
hence seq . (n + 1) < seq . n by A6; :: thesis: verum