theorem :: TSP_2:7
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X holds Cl A = MaxADSet (M /\ (Cl A)) by Th5;