let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset 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 Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A
let A be Subset of X; :: thesis: (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A
reconsider C = the carrier of X0 as non empty Subset of X by TSEP_1:1;
set r = Stone-retraction (X,X0);
C c= the carrier of X ;
then reconsider B = (Stone-retraction (X,X0)) .: A as Subset of X by XBOOLE_1:1;
C /\ (MaxADSet A) = B by Def12;
then A1: B c= MaxADSet A by XBOOLE_1:17;
A2: (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet B by Th26;
then A c= MaxADSet B by FUNCT_2:42;
hence (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A by A2, A1, TEX_4:35; :: thesis: verum