let n be Nat; for r being Real st r is irrational holds
( (scf r) . n < (rfs r) . n & (rfs r) . n < ((scf r) . n) + 1 & 1 < (rfs r) . (n + 1) )
let r be Real; ( r is irrational implies ( (scf r) . n < (rfs r) . n & (rfs r) . n < ((scf r) . n) + 1 & 1 < (rfs r) . (n + 1) ) )
assume
r is irrational
; ( (scf r) . n < (rfs r) . n & (rfs r) . n < ((scf r) . n) + 1 & 1 < (rfs r) . (n + 1) )
then A2:
not (rfs r) . n is integer
by Th2;
A3: 1 / ((rfs r) . (n + 1)) =
1 / (1 / (frac ((rfs r) . n)))
by REAL_3:def 3
.=
frac ((rfs r) . n)
;
A4:
1 / ((rfs r) . (n + 1)) > 0
by A2, A3, INT_1:46;
A5:
(rfs r) . n = ((scf r) . n) + (1 / ((rfs r) . (n + 1)))
by Th1;
A6:
(((rfs r) . n) - ((scf r) . n)) + ((scf r) . n) > 0 + ((scf r) . n)
by A2, A3, A5, INT_1:46, XREAL_1:8;
1 " < (((rfs r) . (n + 1)) ") "
by A3, INT_1:43, A4, XREAL_1:88;
hence
( (scf r) . n < (rfs r) . n & (rfs r) . n < ((scf r) . n) + 1 & 1 < (rfs r) . (n + 1) )
by A6, A5, A3, INT_1:43, XREAL_1:8; verum