let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
let a be Point of X; :: thesis: for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
let b be Point of X0; :: thesis: ( a = b implies (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} )
assume A1: a = b ; :: thesis: (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
Stone-retraction (X,X0) is being_a_retraction by Def9;
hence (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} by A1, Lm2; :: thesis: verum