for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E