theorem Th5: :: TOPALG_1:5

for X being Subset of I[01]
for a being Point of I[01] st X = [.0,a.[ holds
X is open