theorem Th31: :: BORSUK_5:32

for A being Subset of R^1
for a, b being Real st a < b & A = IRRAT (a,b) holds
Cl A = [.a,b.]