theorem Th9: :: TSEP_1:9

for X being TopSpace
for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( B is open iff A is open )