let X be non empty TopSpace; 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; 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 S1[ 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 S1[x,a]
proof
let x be
Point of
X;
ex a being Point of X0 st S1[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
;
S1[x,a]
thus
S1[
x,
a]
by A4;
verum
end;
consider r being Function of X,X0 such that
A5:
for x being Point of X holds S1[x,r . x]
from FUNCT_2:sch 3(A2);
reconsider r = r as continuous Function of X,X0 by A5, Th18;
take
r
; r is being_a_retraction
thus
r is being_a_retraction
by A5, Th20; verum