let X be non empty TopSpace; :: thesis:
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis:
let r be Function of X,X0; :: thesis:
let M be Subset of X; :: thesis:
assume A1: M = the carrier of X0 ; :: thesis:
reconsider N = M as Subset of X ;
assume A2: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ; :: thesis:
A3: N is maximal_T_0 by A1, Th11;
then A4: N is T_0 ;
for F being Subset of X0 st F is closed holds
r " F is closed

proof

let F be Subset of X0; :: thesis:
reconsider E = F as Subset of X by A1, XBOOLE_1:1;
set R = { (MaxADSet a) where a is Point of X : a in E } ;

now :: thesis:

let x be object ; :: thesis:
assume A5: x in r " F ; :: thesis:
then reconsider b = x as Point of X ;
A6: r . b in F by A5, FUNCT_2:38;
E c= the carrier of X ;
then reconsider a = r . b as Point of X by A6;
MaxADSet a in { (MaxADSet a) where a is Point of X : a in E } by A6;
then A7: MaxADSet a c= union { (MaxADSet a) where a is Point of X : a in E } by ZFMISC_1:74;
M /\ (MaxADSet b) = {a} by A2;
then a in M /\ (MaxADSet b) by ZFMISC_1:31;
then a in MaxADSet b by XBOOLE_0:def 4;
then A8: MaxADSet a = MaxADSet b by TEX_4:21;
A9: {b} c= MaxADSet b by TEX_4:18;
b in {b} by TARSKI:def 1;
then b in MaxADSet a by A8, A9;
hence x in union { (MaxADSet a) where a is Point of X : a in E } by A7; :: thesis:

end;

then A10: r " F c= union { (MaxADSet a) where a is Point of X : a in E } by TARSKI:def 3;
assume F is closed ; :: thesis:
then ex P being Subset of X st
( P is closed & P /\ ([#] X0) = F ) by PRE_TOPC:13;
then A11: MaxADSet E is closed by A1, A3, Th5;

now :: thesis:

let C be set ; :: thesis:
assume C in { (MaxADSet a) where a is Point of X : a in E } ; :: thesis:
then consider a being Point of X such that
A12: C = MaxADSet a and
A13: a in E ;

now :: thesis:

let x be object ; :: thesis:
assume A14: x in C ; :: thesis:
then reconsider b = x as Point of X by A12;
A15: M /\ (MaxADSet b) = {(r . b)} by A2;
A16: M /\ (MaxADSet a) = {a} by A1, A4, A13;
MaxADSet a = MaxADSet b by A12, A14, TEX_4:21;
then a = r . x by A16, A15, ZFMISC_1:3;
hence x in r " F by A12, A13, A14, FUNCT_2:38; :: thesis:

end;

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

end;

then A17: union { (MaxADSet a) where a is Point of X : a in E } c= r " F by ZFMISC_1:76;
union { (MaxADSet a) where a is Point of X : a in E } = MaxADSet E by TEX_4:def 11;
hence r " F is closed by A11, A17, A10, XBOOLE_0:def 10; :: thesis:

end;

hence r is continuous Function of X,X0 by PRE_TOPC:def 6; :: thesis: