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:23; :: thesis: verum