theorem Th25: :: JORDAN2B:25

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