theorem Th15: :: TSEP_1:15

for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is closed holds
ex X0 being non empty strict closed SubSpace of X st A0 = the carrier of X0