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 " {b} = MaxADSet 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 " {b} = MaxADSet 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 " {b} = MaxADSet 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 " {b} = MaxADSet a
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
r " {b} = MaxADSet a
let b be Point of X0; :: thesis: ( a = b implies r " {b} = MaxADSet a )
assume A2: a = b ; :: thesis: r " {b} = MaxADSet a
A3: r " {b} c= MaxADSet a MaxADSet a c= r " {b} by A1, A2, Lm4;
hence r " {b} = MaxADSet a by A3, XBOOLE_0:def 10; :: thesis: verum