let X be non empty TopSpace; for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X st ( A is closed or B is closed ) 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; for A, B being Subset of X st ( A is closed or B is closed ) 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; ( ( A is closed or B is closed ) implies (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) )
assume A1:
( A is closed or B is closed )
; (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:64
.=
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)
; verum