let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a
let a be Point of X; :: thesis: (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction (X,X0);
(Stone-retraction (X,X0)) . a in A ;
then reconsider b = (Stone-retraction (X,X0)) . a as Point of X ;
A1: (Stone-retraction (X,X0)) . a in MaxADSet a by Def11;
(Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet b by Th25;
hence (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a by A1, TEX_4:21; :: thesis: verum