let A be Subset of R^1; :: thesis: ( A = IRRAT implies A is dense )
assume A = IRRAT ; :: thesis: A is dense
then Cl A = the carrier of R^1 by BORSUK_5:51;
hence A is dense by TOPS_3:def 2; :: thesis: verum