let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being Function of X,X0
for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is continuous Function of X,X0
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for r being Function of X,X0
for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is continuous Function of X,X0
let r be Function of X,X0; :: thesis: for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is continuous Function of X,X0
let M be Subset of X; :: thesis: ( M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) implies r is continuous Function of X,X0 )
assume A1: M = the carrier of X0 ; :: thesis: ( ex a being Point of X st not M /\ (MaxADSet a) = {(r . a)} or r is continuous Function of X,X0 )
reconsider N = M as Subset of X ;
assume A2: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ; :: thesis: r is continuous Function of X,X0
A3: N is maximal_T_0 by A1, Th11;
then A4: N is T_0 by Def4;
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 )
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

let x be set ; :: thesis: ( x in r " F implies x in union { (MaxADSet a) where a is Point of X : a in E } )
assume A5: x in r " F ; :: thesis: x in union { (MaxADSet a) where a is Point of X : a in E }
then reconsider b = x as Point of X ;
A6: r . b in F by A5, FUNCT_2:46;
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:92;
M /\ (MaxADSet b) = {a} by A2;
then a in M /\ (MaxADSet b) by ZFMISC_1:37;
then a in MaxADSet b by XBOOLE_0:def 4;
then A8: MaxADSet a = MaxADSet b by TEX_4:23;
A9: {b} c= MaxADSet b by TEX_4:20;
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: verum

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: r " F is closed
then ex P being Subset of X st
( P is closed & P /\ ([#] X0) = F ) by PRE_TOPC:43;
then A11: MaxADSet E is closed by A1, A3, Th5;

now

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

now

let x be set ; :: thesis: ( x in C implies x in r " F )
assume A14: x in C ; :: thesis: x in r " F
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, Def2;
MaxADSet a = MaxADSet b by A12, A14, TEX_4:23;
then a = r . x by A16, A15, ZFMISC_1:6;
hence x in r " F by A12, A13, A14, FUNCT_2:46; :: thesis: verum

end;

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

end;

then A17: union { (MaxADSet a) where a is Point of X : a in E } c= r " F by ZFMISC_1:94;
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: verum

end;

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