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