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)) " {b} = MaxADSet 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)) " {b} = MaxADSet a
let a be Point of X; :: thesis: for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " {b} = MaxADSet a
let b be Point of X0; :: thesis: ( a = b implies (Stone-retraction (X,X0)) " {b} = MaxADSet a )
assume A1: a = b ; :: thesis: (Stone-retraction (X,X0)) " {b} = MaxADSet a
Stone-retraction (X,X0) is being_a_retraction by Def9;
hence (Stone-retraction (X,X0)) " {b} = MaxADSet a by A1, Lm5; :: thesis: verum