for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a)