let r be Real; :: thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies r is irrational )
assume A1: for n being Nat holds (scf r) . n <> 0 ; :: thesis: r is irrational
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 r is irrational by Th42; :: thesis: verum