let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X ex r being continuous Function of X,X0 st r is being_a_retraction
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: ex r being continuous Function of X,X0 st r is being_a_retraction
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
defpred S₁[ Point of X, set ] means M /\ (MaxADSet $1) = {$2};
A1: M is maximal_T_0 by Th11;
A2: for x being Point of X ex a being Point of X0 st S₁[x,a]

proof

let x be Point of X; :: thesis: ex a being Point of X0 st S₁[x,a]
consider a being Point of X such that
A3: a in M and
A4: M /\ (MaxADSet x) = {a} by A1;
reconsider a = a as Point of X0 by A3;
take a ; :: thesis: S₁[x,a]
thus S₁[x,a] by A4; :: thesis: verum

end;

consider r being Function of X,X0 such that
A5: for x being Point of X holds S₁[x,r . x] from FUNCT_2:sch 3(A2);
reconsider r = r as continuous Function of X,X0 by A5, Th18;
take r ; :: thesis: r is being_a_retraction
thus r is being_a_retraction by A5, Th20; :: thesis: verum