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