let X be non empty discrete TopSpace; :: thesis: for X0 being non empty SubSpace of X holds X0 is_a_retract_of X
let X0 be non empty 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 Th66;
hence X0 is_a_retract_of X by BORSUK_1:def 17; :: thesis: verum