for r being irrational Real holds frac r is irrational ;