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

proof

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

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 + k) <= seq . ((n + k) + 1) by A1;
hence S₁[k + 1] by A3, XXREAL_0:2; :: thesis: verum

end;

A4: S₁[ 0 ] ;
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 <= seq . (n + k) ) implies for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) :: thesis: ( ( for n, m being Element of NAT st n <= m holds
seq . n <= seq . m ) implies for n being Element of NAT holds seq . n <= seq . (n + 1) )

proof

assume A5: for n, k being Element of NAT holds seq . n <= seq . (n + k) ; :: thesis: for n, m being Element of NAT st n <= m holds
seq . n <= seq . m
let n, m be Element of NAT ; :: thesis: ( n <= m implies seq . n <= seq . m )
assume n <= m ; :: thesis: seq . n <= seq . m
then consider k1 being Nat such that
A6: m = n + k1 by NAT_1:10;
k1 in NAT by ORDINAL1:def 13;
hence seq . n <= seq . m by A5, A6; :: thesis: verum

end;

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