let n be Nat; :: thesis: for r being Real st n >= 1 & (scf r) . n <> 0 holds
(scf r) . n >= 1
let r be Real; :: thesis: ( n >= 1 & (scf r) . n <> 0 implies (scf r) . n >= 1 )
assume ( n >= 1 & (scf r) . n <> 0 ) ; :: thesis: (scf r) . n >= 1
then (scf r) . n > 0 by Th38;
then (scf r) . n >= 0 + 1 by INT_1:7;
hence (scf r) . n >= 1 ; :: thesis: verum