theorem Th27: :: ISOMICHI:27

for A being Subset of R^1
for a, b being Real st A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ holds
Cl A = the carrier of R^1