theorem :: TSP_2:13

for X being non empty TopSpace
for Y0 being non empty T_0 SubSpace of X ex X0 being strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_T_0 )