:: deftheorem Def10 defines Stone-retraction TSP_2:def 10 :
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b3 being continuous Function of X,X0 holds
( b3 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(b3 . a)} );