theorem Th27: :: TSP_2:27

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