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) .: A = (Stone-retraction X,X0) .: (MaxADSet A)
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for A being Subset of X holds (Stone-retraction X,X0) .: A = (Stone-retraction X,X0) .: (MaxADSet A)
let A be Subset of X; :: thesis: (Stone-retraction X,X0) .: A = (Stone-retraction X,X0) .: (MaxADSet A)
set r = Stone-retraction X,X0;
A1: ( A c= the carrier of X & rng (Stone-retraction X,X0) = (Stone-retraction X,X0) .: the carrier of X ) by FUNCT_2:45;
(Stone-retraction X,X0) .: ((Stone-retraction X,X0) " ((Stone-retraction X,X0) .: A)) = (Stone-retraction X,X0) .: (MaxADSet A) by Th29;
hence (Stone-retraction X,X0) .: A = (Stone-retraction X,X0) .: (MaxADSet A) by A1, FUNCT_1:147, RELAT_1:156; :: thesis: verum