theorem Th4: :: TOPALG_1:4

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