theorem :: TSP_2:17

for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for F being Subset of X holds
( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) )