let X be non empty almost_discrete TopSpace; :: thesis: for X0 being non empty maximal_discrete SubSpace of X holds X0 is_a_retract_of X
let X0 be non empty maximal_discrete SubSpace of X; :: thesis: X0 is_a_retract_of X
ex r being continuous Function of X,X0 st r is being_a_retraction by Th68;
hence X0 is_a_retract_of X by BORSUK_1:def 17; :: thesis: verum