theorem Th27: :: BORSUK_5:28
for A being Subset of R^1 st A = IRRAT holds
Cl A = the carrier of R^1