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

proof

let x be Point of X; :: thesis: ( x in the carrier of X0 implies r . x = x )
assume x in the carrier of X0 ; :: thesis: r . x = x
then ( M /\ (MaxADSet x) = {(r . x)} & M /\ (MaxADSet x) = {x} ) by A1, A2, A3, Def2;
hence r . x = x by ZFMISC_1:6; :: thesis: verum

end;

hence r is being_a_retraction by BORSUK_1:def 19; :: thesis: verum