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 )
reconsider N = M as Subset of X ;
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 )
then N is maximal_T_0 by Th11;
then A2: N is T_0 ;
assume A3: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ; :: thesis: r is being_a_retraction
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 A4: M /\ (MaxADSet x) = {x} by A1, A2;
M /\ (MaxADSet x) = {(r . x)} by A3;
hence r . x = x by A4, ZFMISC_1:3; :: thesis: verum

end;

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