theorem Th3: :: TOPALG_1:3

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