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}
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
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}
assume not MaxADSet a c= r " {b} ; :: thesis: contradiction
then consider s being object such that
A3: s in MaxADSet a and
A4: not s in r " {b} by TARSKI:def 3;
reconsider s = s as Point of X by A3;
A5: MaxADSet a = MaxADSet s by A3, TEX_4:21;
A6: {s} c= MaxADSet s by TEX_4:18;
A7: r " (Cl {b}) = Cl {a} by A1, A2, Lm2;
then {a} c= r " (Cl {b}) by PRE_TOPC:18;
then a in r " (Cl {b}) by ZFMISC_1:31;
then MaxADSet s c= r " (Cl {b}) by A7, A5, TEX_4:23;
then {s} c= r " (Cl {b}) by A6, XBOOLE_1:1;
then s in r " (Cl {b}) by ZFMISC_1:31;
then A8: r . s in Cl {b} by FUNCT_2:38;
A c= the carrier of X ;
then reconsider d = r . s as Point of X by TARSKI:def 3;
{(r . s)} c= Cl {(r . s)} by PRE_TOPC:18;
then A9: r . s in Cl {(r . s)} by ZFMISC_1:31;
A10: {a} c= MaxADSet a by TEX_4:18;
r " (Cl {(r . s)}) = Cl {d} by A1, Lm2;
then s in Cl {d} by A9, FUNCT_2:38;
then MaxADSet a c= Cl {d} by A5, TEX_4:23;
then {a} c= Cl {d} by A10, XBOOLE_1:1;
then A11: Cl {a} c= Cl {d} by TOPS_1:5;
Cl {b} c= Cl {a} by A2, TOPS_3:53;
then {d} c= Cl {a} by A8, ZFMISC_1:31;
then Cl {d} c= Cl {a} by TOPS_1:5;
then Cl {d} = Cl {a} by A11, XBOOLE_0:def 10;
then A12: MaxADSet d = MaxADSet a by TEX_4:49;
A is maximal_T_0 by Th11;
then A13: A is T_0 ;
r . a = b by A1, A2, BORSUK_1:def 16;
then A /\ (MaxADSet a) = {b} by A1, Lm3;
then {b} = {(r . s)} by A13, A12;
then r . s in {b} by ZFMISC_1:31;
hence contradiction by A4, FUNCT_2:38; :: thesis: verum