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:38
.= (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