let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X st A is closed holds
(Stone-retraction (X,X0)) .: A is closed
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for A being Subset of X st A is closed holds
(Stone-retraction (X,X0)) .: A is closed
let A be Subset of X; :: thesis: ( A is closed implies (Stone-retraction (X,X0)) .: A is closed )
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set B = (Stone-retraction (X,X0)) .: A;
assume A1: A is closed ; :: thesis: (Stone-retraction (X,X0)) .: A is closed
then A = MaxADSet A by TEX_4:60;
then A /\ M = (Stone-retraction (X,X0)) .: A by Def12;
hence (Stone-retraction (X,X0)) .: A is closed by A1, TSP_1:def 2; :: thesis: verum