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
MaxADSet a c= r " {b}
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
MaxADSet a c= r " {b}
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
MaxADSet a c= r " {b} )
assume A1: r is being_a_retraction ; :: thesis: for a being Point of X
for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
let a be Point of X; :: thesis: for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
let b be Point of X0; :: thesis: ( a = b implies MaxADSet a c= r " {b} )
assume A2: a = b ; :: thesis: MaxADSet a c= r " {b}
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A is maximal_T_0 by Th11;
then A3: A is T_0 by Def4;
r . a = b by A1, A2, BORSUK_1:def 19;
then A4: A /\ (MaxADSet a) = {b} by A1, Lm3;
assume not MaxADSet a c= r " {b} ; :: thesis: contradiction
then consider s being set such that
A5: s in MaxADSet a and
A6: not s in r " {b} by TARSKI:def 3;
reconsider s = s as Point of X by A5;
A7: r " (Cl {b}) = Cl {a} by A1, A2, Lm2;
A c= the carrier of X ;
then reconsider d = r . s as Point of X by TARSKI:def 3;
A8: r " (Cl {(r . s)}) = Cl {d} by A1, Lm2;
{(r . s)} c= Cl {(r . s)} by PRE_TOPC:48;
then r . s in Cl {(r . s)} by ZFMISC_1:37;
then A9: s in Cl {d} by A8, FUNCT_2:46;
A10: MaxADSet a = MaxADSet s by A5, TEX_4:23;
then A11: MaxADSet a c= Cl {d} by A9, TEX_4:25;
{a} c= MaxADSet a by TEX_4:20;
then {a} c= Cl {d} by A11, XBOOLE_1:1;
then A12: Cl {a} c= Cl {d} by TOPS_1:31;
A13: {s} c= MaxADSet s by TEX_4:20;
{a} c= r " (Cl {b}) by A7, PRE_TOPC:48;
then a in r " (Cl {b}) by ZFMISC_1:37;
then MaxADSet s c= r " (Cl {b}) by A7, A10, TEX_4:25;
then {s} c= r " (Cl {b}) by A13, XBOOLE_1:1;
then s in r " (Cl {b}) by ZFMISC_1:37;
then A14: r . s in Cl {b} by FUNCT_2:46;
Cl {b} c= Cl {a} by A2, TOPS_3:53;
then {d} c= Cl {a} by A14, ZFMISC_1:37;
then Cl {d} c= Cl {a} by TOPS_1:31;
then Cl {d} = Cl {a} by A12, XBOOLE_0:def 10;
then MaxADSet d = MaxADSet a by TEX_4:51;
then {b} = {(r . s)} by A3, A4, Def2;
then r . s in {b} by ZFMISC_1:37;
hence contradiction by A6, FUNCT_2:46; :: thesis: verum