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 Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . 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 Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
let r be continuous Function of X,X0; :: thesis: ( r is being_a_retraction implies for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} )
assume A1: r is being_a_retraction ; :: thesis: for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
let A be Subset of X; :: thesis: ( A = the carrier of X0 implies for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} )
reconsider N = A as Subset of X ;
assume A2: A = the carrier of X0 ; :: thesis: for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
let a be Point of X; :: thesis: A /\ (MaxADSet a) = {(r . a)}
A3: N is maximal_T_0 by A2, Th11;
then consider c being Point of X such that
A4: c in A and
A5: A /\ (MaxADSet a) = {c} ;
A6: {c} c= MaxADSet c by TEX_4:18;
r . a in A by A2;
then reconsider d = r . a as Point of X ;
{(r . a)} c= Cl {(r . a)} by PRE_TOPC:18;
then A7: r . a in Cl {(r . a)} by ZFMISC_1:31;
{c} c= MaxADSet a by A5, XBOOLE_1:17;
then c in MaxADSet a by ZFMISC_1:31;
then A8: MaxADSet c = MaxADSet a by TEX_4:21;
reconsider b = c as Point of X0 by A2, A4;
A9: {a} c= MaxADSet a by TEX_4:18;
A10: r " (Cl {b}) = Cl {c} by A1, Lm2;
then {c} c= r " (Cl {b}) by PRE_TOPC:18;
then c in r " (Cl {b}) by ZFMISC_1:31;
then MaxADSet a c= r " (Cl {b}) by A10, A8, TEX_4:23;
then {a} c= r " (Cl {b}) by A9, XBOOLE_1:1;
then a in r " (Cl {b}) by ZFMISC_1:31;
then A11: r . a in Cl {b} by FUNCT_2:38;
r " (Cl {(r . a)}) = Cl {d} by A1, Lm2;
then a in Cl {d} by A7, FUNCT_2:38;
then MaxADSet c c= Cl {d} by A8, TEX_4:23;
then {c} c= Cl {d} by A6, XBOOLE_1:1;
then A12: Cl {c} c= Cl {d} by TOPS_1:5;
Cl {b} c= Cl {c} by TOPS_3:53;
then {d} c= Cl {c} by A11, ZFMISC_1:31;
then Cl {d} c= Cl {c} by TOPS_1:5;
then Cl {d} = Cl {c} by A12, XBOOLE_0:def 10;
then A13: MaxADSet d = MaxADSet a by A8, TEX_4:49;
N is T_0 by A3;
hence A /\ (MaxADSet a) = {(r . a)} by A2, A13; :: thesis: verum