theorem :: ISOMICHI:30

for a, b being Real st a >= b holds
IRRAT (a,b) = {}