for A being Subset of R^1 st A = IRRAT holds
A ` = RAT by Lm2, TOPMETR:17;