for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for E being Subset of X
for F being Subset of X0 st F = E holds
(Stone-retraction (X,X0)) " F = MaxADSet E by Def9, Lm6;