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: rng (Stone-retraction (X,X0)) = (Stone-retraction (X,X0)) .: the carrier of X by RELSET_1:22;
(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:77, RELAT_1:123; :: thesis: verum