let r be real number ; :: thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies not r is rational )
assume A1: for n being Nat holds (scf r) . n <> 0 ; :: thesis: not r is rational
for n being Nat ex m being Nat st
( m >= n & not (scf r) . m = 0 )

proof

let n be Nat; :: thesis: ex m being Nat st
( m >= n & not (scf r) . m = 0 )
take n ; :: thesis: ( n >= n & not (scf r) . n = 0 )
thus ( n >= n & not (scf r) . n = 0 ) by A1; :: thesis: verum

end;

hence not r is rational by Th42; :: thesis: verum