theorem Th5: :: TSP_2:5

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 st A is closed holds
A = MaxADSet (M /\ A)