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 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
let r be continuous Function of X,X0; :: thesis: ( r is being_a_retraction implies for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a )
assume A1: r is being_a_retraction ; :: thesis: for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let a be Point of X; :: thesis: for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
let b be Point of X0; :: thesis: ( a = b implies r " {b} = MaxADSet a )
assume A2: a = b ; :: thesis: r " {b} = MaxADSet a
A3: r " {b} c= MaxADSet a

proof

assume not r " {b} c= MaxADSet a ; :: thesis: contradiction
then consider s being object such that
A4: s in r " {b} and
A5: not s in MaxADSet a by TARSKI:def 3;
reconsider s = s as Point of X by A4;
r . s in {b} by A4, FUNCT_2:38;
then {(r . s)} c= {b} by ZFMISC_1:31;
then {(r . s)} = {b} by ZFMISC_1:18;
then A /\ (MaxADSet s) = {b} by A1, Lm3;
then {a} c= MaxADSet s by A2, XBOOLE_1:17;
then a in MaxADSet s by ZFMISC_1:31;
then A6: MaxADSet s = MaxADSet a by TEX_4:21;
{s} c= MaxADSet s by TEX_4:18;
hence contradiction by A5, A6, ZFMISC_1:31; :: thesis: verum

end;

MaxADSet a c= r " {b} by A1, A2, Lm4;
hence r " {b} = MaxADSet a by A3, XBOOLE_0:def 10; :: thesis: verum