for r being Real holds
( [\r/] = r iff r is integer )