let n be Nat; for r being Real st r is irrational holds
0 < (scf r) . (n + 1)
let r be Real; ( r is irrational implies 0 < (scf r) . (n + 1) )
assume A1:
r is irrational
; 0 < (scf r) . (n + 1)
A2:
((rfs r) . (n + 1)) - 1 > 1 - 1
by A1, Th4, XREAL_1:14;
(rfs r) . (n + 1) < ((scf r) . (n + 1)) + 1
by A1, Th4;
then
((rfs r) . (n + 1)) - 1 < (((scf r) . (n + 1)) + 1) - 1
by XREAL_1:14;
hence
0 < (scf r) . (n + 1)
by A2; verum