theorem Th12: :: JORDAN20:12

for P being Subset of I[01]
for s being Real st P = ].s,1.] holds
P is open