for a, b being Real holds IRRAT (a,b) misses RAT (a,b)