let A be Subset of R^1; :: thesis: ( A = IRRAT implies Int A = {} )
assume A = IRRAT ; :: thesis: Int A = {}
then Cl (A `) = [#] R^1 by Lm2, BORSUK_5:15, TOPMETR:17;
then (Cl (A `)) ` = {} R^1 by XBOOLE_1:37;
hence Int A = {} by Th3; :: thesis: verum