let A be Subset of R^1 ; :: thesis: ( A = RAT implies Int A = {} )
assume A = RAT ; :: thesis: Int A = {}
then Cl (A ` ) = [#] R^1 by BORSUK_5:51, BORSUK_5:def 3, TOPMETR:24;
then (Cl (A ` )) ` = {} R^1 by XBOOLE_1:37;
hence Int A = {} by Th5; :: thesis: verum