let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X holds Im (Stone-retraction X,X0),a = (Stone-retraction X,X0) .: (MaxADSet a)
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for a being Point of X holds Im (Stone-retraction X,X0),a = (Stone-retraction X,X0) .: (MaxADSet a)
let a be Point of X; :: thesis: Im (Stone-retraction X,X0),a = (Stone-retraction X,X0) .: (MaxADSet a)
set r = Stone-retraction X,X0;
A1: dom (Stone-retraction X,X0) = [#] X by FUNCT_2:def 1;
A2: (Stone-retraction X,X0) .: ((Stone-retraction X,X0) " {((Stone-retraction X,X0) . a)}) c= {((Stone-retraction X,X0) . a)} by FUNCT_1:145;
A3: (Stone-retraction X,X0) " {((Stone-retraction X,X0) . a)} = MaxADSet a by Th27;
then (Stone-retraction X,X0) .: ((Stone-retraction X,X0) " {((Stone-retraction X,X0) . a)}) <> {} by A1, RELAT_1:152;
then (Stone-retraction X,X0) .: ((Stone-retraction X,X0) " {((Stone-retraction X,X0) . a)}) = {((Stone-retraction X,X0) . a)} by A2, ZFMISC_1:39;
hence Im (Stone-retraction X,X0),a = (Stone-retraction X,X0) .: (MaxADSet a) by A1, A3, FUNCT_1:117; :: thesis: verum