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 )
assume A2: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ; :: thesis: r is continuous Function of X,X0
reconsider N = M as Subset of X ;
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 )
assume A5: F is closed ; :: thesis: r " F is closed
reconsider E = F as Subset of X by A1, XBOOLE_1:1;
consider P being Subset of X such that
A6: P is closed and
A7: P /\ ([#] X0) = F by A5, PRE_TOPC:43;
set R = { (MaxADSet a) where a is Point of X : a in E } ;
A8: union { (MaxADSet a) where a is Point of X : a in E } = MaxADSet E by TEX_4:def 11;
A9: MaxADSet E is closed by A1, A3, A6, A7, Th5;
A10: union { (MaxADSet a) where a is Point of X : a in E } c= r " F

proof

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
A11: C = MaxADSet a and
A12: a in E ;

now

let x be set ; :: thesis: ( x in C implies x in r " F )
assume A13: x in C ; :: thesis: x in r " F
then reconsider b = x as Point of X by A11;
A14: MaxADSet a = MaxADSet b by A11, A13, TEX_4:23;
A15: M /\ (MaxADSet a) = {a} by A1, A4, A12, Def2;
M /\ (MaxADSet b) = {(r . b)} by A2;
then a = r . x by A14, A15, ZFMISC_1:6;
hence x in r " F by A11, A12, A13, FUNCT_2:46; :: thesis: verum

end;

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

end;

hence union { (MaxADSet a) where a is Point of X : a in E } c= r " F by ZFMISC_1:94; :: thesis: verum

end;

r " F c= union { (MaxADSet a) where a is Point of X : a in E }

proof

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 A16: 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 ;
A17: r . b in F by A16, FUNCT_2:46;
E c= the carrier of X ;
then reconsider a = r . b as Point of X by A17;
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 A18: MaxADSet a = MaxADSet b by TEX_4:23;
MaxADSet a in { (MaxADSet a) where a is Point of X : a in E } by A17;
then A19: MaxADSet a c= union { (MaxADSet a) where a is Point of X : a in E } by ZFMISC_1:92;
( b in {b} & {b} c= MaxADSet b ) by TARSKI:def 1, TEX_4:20;
then b in MaxADSet a by A18;
hence x in union { (MaxADSet a) where a is Point of X : a in E } by A19; :: thesis: verum

end;

hence r " F c= union { (MaxADSet a) where a is Point of X : a in E } by TARSKI:def 3; :: thesis: verum

end;

hence r " F is closed by A8, A9, A10, XBOOLE_0:def 10; :: thesis: verum

end;

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