let X be non empty TopSpace; 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; 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; ( 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
; for a being Point of X
for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let a be Point of X; for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
let b be Point of X0; ( a = b implies r " (Cl {b}) = Cl {a} )
A2:
b in {b}
by TARSKI:def 1;
assume A3:
a = b
; r " (Cl {b}) = Cl {a}
then
r . a = b
by A1, BORSUK_1:def 16;
then A4:
a in r " {b}
by A2, FUNCT_2:38;
A5:
A is maximal_T_0
by Th11;
A6:
r " (Cl {b}) c= Cl {a}
proof
assume
not
r " (Cl {b}) c= Cl {a}
;
contradiction
then consider c being
object 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;
consider d being
Point of
X such that A9:
d in A
and A10:
A /\ (MaxADSet c) = {d}
by A5;
A11:
{d} c= MaxADSet c
by A10, XBOOLE_1:17;
r " (Cl {b}) is
closed
by PRE_TOPC:def 6;
then
MaxADSet c c= r " (Cl {b})
by A7, TEX_4:23;
then
{d} c= r " (Cl {b})
by A11, XBOOLE_1:1;
then A12:
d in r " (Cl {b})
by ZFMISC_1:31;
reconsider e =
d as
Point of
X0 by A9;
{c} c= MaxADSet c
by TEX_4:18;
then A13:
c in MaxADSet c
by ZFMISC_1:31;
A14:
Cl {b} c= Cl {a}
by A3, TOPS_3:53;
r . d = e
by A1, BORSUK_1:def 16;
then
e in Cl {b}
by A12, FUNCT_2:38;
then A15:
MaxADSet d c= Cl {a}
by A14, TEX_4:23;
d in MaxADSet c
by A11, ZFMISC_1:31;
then
MaxADSet d = MaxADSet c
by TEX_4:21;
hence
contradiction
by A8, A13, A15;
verum
end;
A16:
r " (Cl {b}) is closed
by PRE_TOPC:def 6;
r " {b} c= r " (Cl {b})
by PRE_TOPC:18, RELAT_1:143;
then
{a} c= r " (Cl {b})
by A4, ZFMISC_1:31;
then
Cl {a} c= r " (Cl {b})
by A16, TOPS_1:5;
hence
r " (Cl {b}) = Cl {a}
by A6, XBOOLE_0:def 10; verum