let X be non empty almost_discrete TopSpace; :: thesis: for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}
let X0 be non empty maximal_discrete SubSpace of X; :: thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}
let r be continuous Function of X,X0; :: thesis: ( r is being_a_retraction implies for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a} )
assume A1: r is being_a_retraction ; :: thesis: for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}
let a be Point of X0; :: thesis: for b being Point of X st a = b holds
Cl {b} c= r " {a}
let b be Point of X; :: thesis: ( a = b implies Cl {b} c= r " {a} )
assume a = b ; :: thesis: Cl {b} c= r " {a}
then A2: r . b = a by A1, BORSUK_1:def 16;
a in {a} by TARSKI:def 1;
then b in r " {a} by A2, FUNCT_2:38;
then A3: {b} c= r " {a} by ZFMISC_1:31;
{a} is closed by TDLAT_3:16;
then r " {a} is closed by PRE_TOPC:def 6;
hence Cl {b} c= r " {a} by A3, TOPS_1:5; :: thesis: verum