theorem Th9: :: TSP_2:9

for X being non empty TopSpace
for A being Subset of X st A is T_0 holds
ex M being Subset of X st
( A c= M & M is maximal_T_0 )