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 open holds
(Stone-retraction (X,X0)) .: A is open
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for A being Subset of X st A is open holds
(Stone-retraction (X,X0)) .: A is open
let A be Subset of X; :: thesis: ( A is open implies (Stone-retraction (X,X0)) .: A is open )
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 open ; :: thesis: (Stone-retraction (X,X0)) .: A is open
then A = MaxADSet A by TEX_4:56;
then A /\ M = (Stone-retraction (X,X0)) .: A by Def12;
hence (Stone-retraction (X,X0)) .: A is open by A1, TSP_1:def 1; :: thesis: verum