let n be Nat; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( (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; :: thesis: verum