theorem Th24: :: JORDAN2B:24

for P being Subset of R^1
for b being Real st P = { s where s is Real : s < b } holds
P is open