theorem :: REAL_3:43

for r being Real st ( for n being Nat holds (scf r) . n <> 0 ) holds
r is irrational