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:75;
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:119;
then (Stone-retraction (X,X0)) .: ((Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)}) = {((Stone-retraction (X,X0)) . a)} by A2, ZFMISC_1:33;
hence Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a) by A1, A3, FUNCT_1:59; :: thesis: verum