let X be non empty TopSpace; 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; 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; 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; verum