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 Lm3, BORSUK_5:35, TOPMETR:24;
then (Cl (A ` )) ` = {} R^1 by XBOOLE_1:37;
hence Int A = {} by Th5; :: thesis: verum