let X be non empty almost_discrete TopSpace; :: thesis: for X0 being non empty maximal_discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction
let X0 be non empty maximal_discrete SubSpace of X; :: thesis: ex r being continuous Function of X,X0 st r is being_a_retraction
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
defpred S₁[ Point of X, Point of X0] means A /\ (Cl {$1}) = {$2};
A1: A is maximal_discrete by Th45;
then A2: A is discrete ;
A3: 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
A4: a in A and
A5: A /\ (Cl {x}) = {a} by A1, Th58;
reconsider a = a as Point of X0 by A4;
take a ; :: thesis: S₁[x,a]
thus S₁[x,a] by A5; :: thesis: verum

end;

consider r being Function of X,X0 such that
A6: for x being Point of X holds S₁[x,r . x] from FUNCT_2:sch 3(A3);
for F being Subset of X0 st F is closed holds
r " F is closed

proof

let F be Subset of X0; :: thesis: ( F is closed implies r " F is closed )
assume F is closed ; :: thesis: r " F is closed
F c= A ;
then reconsider E = F as Subset of X by XBOOLE_1:1;
set R = { (Cl {a}) where a is Point of X : a in E } ;

now :: thesis: for x being object st x in r " F holds
x in union { (Cl {a}) where a is Point of X : a in E }

let x be object ; :: thesis: ( x in r " F implies x in union { (Cl {a}) where a is Point of X : a in E } )
assume A7: x in r " F ; :: thesis: x in union { (Cl {a}) where a is Point of X : a in E }
then reconsider b = x as Point of X ;
A8: r . b in F by A7, FUNCT_2:38;
E c= the carrier of X ;
then reconsider a = r . b as Point of X by A8;
Cl {a} in { (Cl {a}) where a is Point of X : a in E } by A8;
then A9: Cl {a} c= union { (Cl {a}) where a is Point of X : a in E } by ZFMISC_1:74;
A /\ (Cl {b}) = {a} by A6;
then a in A /\ (Cl {b}) by ZFMISC_1:31;
then a in Cl {b} by XBOOLE_0:def 4;
then A10: Cl {a} = Cl {b} by Th49;
A11: {b} c= Cl {b} by PRE_TOPC:18;
b in {b} by TARSKI:def 1;
then b in Cl {a} by A10, A11;
hence x in union { (Cl {a}) where a is Point of X : a in E } by A9; :: thesis: verum

end;

then A12: r " F c= union { (Cl {a}) where a is Point of X : a in E } by TARSKI:def 3;

now :: thesis: for C being set st C in { (Cl {a}) where a is Point of X : a in E } holds
C c= r " F

let C be set ; :: thesis: ( C in { (Cl {a}) where a is Point of X : a in E } implies C c= r " F )
assume C in { (Cl {a}) where a is Point of X : a in E } ; :: thesis: C c= r " F
then consider a being Point of X such that
A13: C = Cl {a} and
A14: a in E ;

now :: thesis: for x being object st x in C holds
x in r " F

let x be object ; :: thesis: ( x in C implies x in r " F )
assume A15: x in C ; :: thesis: x in r " F
then reconsider b = x as Point of X by A13;
A16: A /\ (Cl {b}) = {(r . b)} by A6;
A17: A /\ (Cl {a}) = {a} by A2, A14, Th36;
Cl {a} = Cl {b} by A13, A15, Th49;
then a = r . x by A17, A16, ZFMISC_1:3;
hence x in r " F by A13, A14, A15, FUNCT_2:38; :: thesis: verum

end;

hence C c= r " F by TARSKI:def 3; :: thesis: verum

end;

then A18: union { (Cl {a}) where a is Point of X : a in E } c= r " F by ZFMISC_1:76;
Cl E = union { (Cl {a}) where a is Point of X : a in E } by Th48;
hence r " F is closed by A18, A12, XBOOLE_0:def 10; :: thesis: verum

end;

then reconsider r = r as continuous Function of X,X0 by PRE_TOPC:def 6;
take r ; :: thesis: r is being_a_retraction
for x being Point of X st x in the carrier of X0 holds
r . x = x

proof

let x be Point of X; :: thesis: ( x in the carrier of X0 implies r . x = x )
assume x in the carrier of X0 ; :: thesis: r . x = x
then A19: A /\ (Cl {x}) = {x} by A2, Th36;
A /\ (Cl {x}) = {(r . x)} by A6;
hence r . x = x by A19, ZFMISC_1:3; :: thesis: verum

end;

hence r is being_a_retraction by BORSUK_1:def 16; :: thesis: verum