let n be Nat; :: thesis: for r being real number st n >= 1 & (scf r) . n <> 0 holds
(scf r) . n >= 1
let r be real number ; :: thesis: ( n >= 1 & (scf r) . n <> 0 implies (scf r) . n >= 1 )
assume that
A1: n >= 1 and
A2: (scf r) . n <> 0 ; :: thesis: (scf r) . n >= 1
(scf r) . n > 0 by A1, A2, Th38;
then (scf r) . n >= 0 + 1 by INT_1:20;
hence (scf r) . n >= 1 ; :: thesis: verum