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) . a)} = MaxADSet a by Th27;
then ( (Stone-retraction X,X0) .: ((Stone-retraction X,X0) " {((Stone-retraction X,X0) . a)}) c= {((Stone-retraction X,X0) . a)} & (Stone-retraction X,X0) .: ((Stone-retraction X,X0) " {((Stone-retraction X,X0) . a)}) <> {} ) by A1, FUNCT_1:145, RELAT_1:152;
then (Stone-retraction X,X0) .: ((Stone-retraction X,X0) " {((Stone-retraction X,X0) . a)}) = {((Stone-retraction X,X0) . a)} by ZFMISC_1:39;
hence Im (Stone-retraction X,X0),a = (Stone-retraction X,X0) .: (MaxADSet a) by A1, A2, FUNCT_1:117; :: thesis: verum