let seq be Real_Sequence; ( ( ( for n being Nat holds seq . n <= seq . (n + 1) ) implies for n, k being Nat holds seq . n <= seq . (n + k) ) & ( ( for n, k being Nat holds seq . n <= seq . (n + k) ) implies for n, m being Nat st n <= m holds
seq . n <= seq . m ) & ( ( for n, m being Nat st n <= m holds
seq . n <= seq . m ) implies for n being Nat holds seq . n <= seq . (n + 1) ) )
thus
( ( for n being Nat holds seq . n <= seq . (n + 1) ) implies for n, k being Nat holds seq . n <= seq . (n + k) )
( ( ( for n, k being Nat holds seq . n <= seq . (n + k) ) implies for n, m being Nat st n <= m holds
seq . n <= seq . m ) & ( ( for n, m being Nat st n <= m holds
seq . n <= seq . m ) implies for n being Nat holds seq . n <= seq . (n + 1) ) )proof
assume A1:
for
n being
Nat holds
seq . n <= seq . (n + 1)
;
for n, k being Nat holds seq . n <= seq . (n + k)
let n be
Nat;
for k being Nat holds seq . n <= seq . (n + k)
defpred S1[
Nat]
means seq . n <= seq . (n + $1);
A2:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A3:
S1[
k]
;
S1[k + 1]
seq . (n + k) <= seq . ((n + k) + 1)
by A1;
hence
S1[
k + 1]
by A3, XXREAL_0:2;
verum end;
A4:
S1[
0 ]
;
thus
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A4, A2); verum
end;
thus
( ( for n, k being Nat holds seq . n <= seq . (n + k) ) implies for n, m being Nat st n <= m holds
seq . n <= seq . m )
( ( for n, m being Nat st n <= m holds
seq . n <= seq . m ) implies for n being Nat holds seq . n <= seq . (n + 1) )proof
assume A5:
for
n,
k being
Nat holds
seq . n <= seq . (n + k)
;
for n, m being Nat st n <= m holds
seq . n <= seq . m
let n,
m be
Nat;
( n <= m implies seq . n <= seq . m )
assume
n <= m
;
seq . n <= seq . m
then consider k1 being
Nat such that A6:
m = n + k1
by NAT_1:10;
thus
seq . n <= seq . m
by A5, A6;
verum
end;
assume A7:
for n, m being Nat st n <= m holds
seq . n <= seq . m
; for n being Nat holds seq . n <= seq . (n + 1)
let n be Nat; seq . n <= seq . (n + 1)
n <= n + 1
by NAT_1:13;
hence
seq . n <= seq . (n + 1)
by A7; verum