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