for a, b being Real holds IRRAT (a,b) c= [.a,+infty.[