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 a being Point of X0
for b being Point of X st a = b holds
r " {a} = Cl {b} by Th70;