let X be non empty almost_discrete TopSpace; :: thesis: for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E
let X0 be non empty maximal_discrete SubSpace of X; :: thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E
let r be continuous Function of X,X0; :: thesis: ( r is being_a_retraction implies for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A1: A is maximal_discrete by Th51;
assume A2: r is being_a_retraction ; :: thesis: for F being Subset of X0
for E being Subset of X st F = E holds
r " F = Cl E
A3: for a being Point of X holds A /\ (Cl {a}) = {(r . a)}

proof

let a be Point of X; :: thesis: A /\ (Cl {a}) = {(r . a)}
A4: {a} c= Cl {a} by PRE_TOPC:18;
consider c being Point of X such that
A5: c in A and
A6: A /\ (Cl {a}) = {c} by A1, Th64;
reconsider b = c as Point of X0 by A5;
{c} c= Cl {a} by A6, XBOOLE_1:17;
then A7: c in Cl {a} by ZFMISC_1:31;
Cl {c} c= r " {b} by A2, Lm4;
then Cl {a} c= r " {b} by A7, Th55;
then {a} c= r " {b} by A4, XBOOLE_1:1;
then a in r " {b} by ZFMISC_1:31;
then r . a in {b} by FUNCT_2:38;
hence A /\ (Cl {a}) = {(r . a)} by A6, TARSKI:def 1; :: thesis: verum

end;

let F be Subset of X0; :: thesis: for E being Subset of X st F = E holds
r " F = Cl E
let E be Subset of X; :: thesis: ( F = E implies r " F = Cl E )
set R = { (Cl {a}) where a is Point of X : a in E } ;
assume A8: F = E ; :: thesis: r " F = Cl E

now

let x be set ; :: thesis: ( x in r " F implies x in union { (Cl {a}) where a is Point of X : a in E } )
assume A9: 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 ;
A10: r . b in F by A9, FUNCT_2:38;
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, A10;
then A11: Cl {a} c= union { (Cl {a}) where a is Point of X : a in E } by ZFMISC_1:74;
A12: {b} c= Cl {b} by PRE_TOPC:18;
A /\ (Cl {b}) = {a} by A3;
then a in A /\ (Cl {b}) by ZFMISC_1:31;
then a in Cl {b} by XBOOLE_0:def 4;
then A13: Cl {a} = Cl {b} by Th55;
b in {b} by TARSKI:def 1;
then b in Cl {a} by A13, A12;
hence x in union { (Cl {a}) where a is Point of X : a in E } by A11; :: thesis: verum

end;

then A14: r " F c= union { (Cl {a}) where a is Point of X : a in E } by TARSKI:def 3;
A15: A is discrete by A1, Def7;

now

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
A16: C = Cl {a} and
A17: a in E ;

now

let x be set ; :: thesis: ( x in C implies x in r " F )
assume A18: x in C ; :: thesis: x in r " F
then reconsider b = x as Point of X by A16;
A19: A /\ (Cl {b}) = {(r . b)} by A3;
A20: A /\ (Cl {a}) = {a} by A8, A15, A17, Th42;
Cl {a} = Cl {b} by A16, A18, Th55;
then a = r . x by A20, A19, ZFMISC_1:3;
hence x in r " F by A8, A16, A17, A18, FUNCT_2:38; :: thesis: verum

end;

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

end;

then A21: 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 Th54;
hence r " F = Cl E by A21, A14, XBOOLE_0:def 10; :: thesis: verum