let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X st ( A is open or B is open ) holds
(Stone-retraction X,X0) .: (A /\ B) = ((Stone-retraction X,X0) .: A) /\ ((Stone-retraction X,X0) .: B)
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: for A, B being Subset of X st ( A is open or B is open ) holds
(Stone-retraction X,X0) .: (A /\ B) = ((Stone-retraction X,X0) .: A) /\ ((Stone-retraction X,X0) .: B)
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
set r = Stone-retraction X,X0;
let A, B be Subset of X; :: thesis: ( ( A is open or B is open ) implies (Stone-retraction X,X0) .: (A /\ B) = ((Stone-retraction X,X0) .: A) /\ ((Stone-retraction X,X0) .: B) )
assume A1: ( A is open or B is open ) ; :: thesis: (Stone-retraction X,X0) .: (A /\ B) = ((Stone-retraction X,X0) .: A) /\ ((Stone-retraction X,X0) .: B)
(Stone-retraction X,X0) .: (A /\ B) = M /\ (MaxADSet (A /\ B)) by Def12
.= (M /\ M) /\ ((MaxADSet A) /\ (MaxADSet B)) by A1, TEX_4:67
.= M /\ (M /\ ((MaxADSet A) /\ (MaxADSet B))) by XBOOLE_1:16
.= ((M /\ (MaxADSet A)) /\ (MaxADSet B)) /\ M by XBOOLE_1:16
.= (M /\ (MaxADSet A)) /\ (M /\ (MaxADSet B)) by XBOOLE_1:16
.= ((Stone-retraction X,X0) .: A) /\ (M /\ (MaxADSet B)) by Def12
.= ((Stone-retraction X,X0) .: A) /\ ((Stone-retraction X,X0) .: B) by Def12 ;
hence (Stone-retraction X,X0) .: (A /\ B) = ((Stone-retraction X,X0) .: A) /\ ((Stone-retraction X,X0) .: B) ; :: thesis: verum