theorem Th2: :: TOPALG_1:2

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