:: deftheorem Def12 defines Stone-retraction TSP_2:def 12 :
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b₃ being continuous Function of X,X0 holds
( b₃ = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = b₃ .: A );