let r be Real; :: thesis: ( r is irrational implies for n being Nat holds (c_d r) . (n + 1) >= (c_d r) . n )
assume A1: r is irrational ; :: thesis: for n being Nat holds (c_d r) . (n + 1) >= (c_d r) . n
defpred S₁[ Nat] means (c_d r) . $1 <= (c_d r) . ($1 + 1);
A2: S₁[ 0 ]

proof

A3: (c_d r) . 0 = 1 by REAL_3:def 6;
(rfs r) . (0 + 1) > 1 by A1, Th4;
then ((rfs r) . 1) - 1 > 1 - 1 by XREAL_1:14;
then [\((rfs r) . 1)/] > 0 by INT_1:def 6;
then (scf r) . 1 > 0 by REAL_3:def 4;
then 0 + 1 <= (scf r) . 1 by INT_1:7;
hence S₁[ 0 ] by A3, REAL_3:def 6; :: thesis: verum

end;

A8: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
A9: ((c_d r) . (n + 2)) - ((c_d r) . (n + 1)) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) - ((c_d r) . (n + 1)) by REAL_3:def 6
.= ((((scf r) . (n + 2)) - 1) * ((c_d r) . (n + 1))) + ((c_d r) . n) ;
A10: (scf r) . (n + 2) = [\((rfs r) . (n + 2))/] by REAL_3:def 4;
(rfs r) . ((n + 1) + 1) > 1 by A1, Th4;
then ((rfs r) . (n + 2)) - 1 > 1 - 1 by XREAL_1:14;
then (scf r) . (n + 2) > 0 by A10, INT_1:def 6;
then 0 + 1 <= (scf r) . (n + 2) by INT_1:7;
then A12: ((scf r) . (n + 2)) - 1 >= 1 - 1 by XREAL_1:13;
( (c_d r) . (n + 1) >= 0 & (c_d r) . n >= 0 ) by REAL_3:51;
then (((c_d r) . (n + 2)) - ((c_d r) . (n + 1))) + ((c_d r) . (n + 1)) >= 0 + ((c_d r) . (n + 1)) by A9, A12, XREAL_1:6;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A8);
hence for n being Nat holds (c_d r) . (n + 1) >= (c_d r) . n ; :: thesis: verum