let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet 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 st ( for a being Point of X holds r . a in MaxADSet a ) holds
r is continuous Function of X,X0
let r be Function of X,X0; :: thesis: ( ( for a being Point of X holds r . a in MaxADSet a ) implies r is continuous Function of X,X0 )
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
assume A1: for a being Point of X holds r . a in MaxADSet a ; :: thesis: r is continuous Function of X,X0
M is maximal_T_0 by Th11;
then A2: M is T_0 ;
A3: M c= the carrier of X ;
for a being Point of X holds M /\ (MaxADSet a) = {(r . a)}
proof
let a be Point of X; :: thesis: M /\ (MaxADSet a) = {(r . a)}
reconsider s = r . a as Point of X by A3, TARSKI:def 3;
A4: s in MaxADSet a by A1;
M /\ (MaxADSet s) = {s} by A2;
hence M /\ (MaxADSet a) = {(r . a)} by A4, TEX_4:21; :: thesis: verum
end;
hence r is continuous Function of X,X0 by Th18; :: thesis: verum