for x being Real holds
( x is irrational iff x in IRRAT )