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