let X be non empty TopSpace; :: thesis: for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X 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 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: (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 /\ ((MaxADSet A) \/ (MaxADSet B)) by TEX_4:36
.= (M /\ (MaxADSet A)) \/ (M /\ (MaxADSet B)) by XBOOLE_1:23
.= ((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