let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is domains-family holds
(union F) \/ (Int (Cl (union F))) is condensed
let F be Subset-Family of T; :: thesis: ( F is domains-family implies (union F) \/ (Int (Cl (union F))) is condensed )
A1: Cl (Int (Cl (union F))) c= Cl (Cl (union F)) by PRE_TOPC:19, TOPS_1:16;
assume F is domains-family ; :: thesis: (union F) \/ (Int (Cl (union F))) is condensed
then union F c= Cl (Int (union F)) by Th65;
then A2: (union F) \/ (Int (Cl (union F))) c= Cl (Int ((union F) \/ (Int (Cl (union F))))) by Th5;
Int (Cl ((union F) \/ (Int (Cl (union F))))) = Int ((Cl (union F)) \/ (Cl (Int (Cl (union F))))) by PRE_TOPC:20
.= Int (Cl (union F)) by A1, XBOOLE_1:12 ;
then Int (Cl ((union F) \/ (Int (Cl (union F))))) c= (union F) \/ (Int (Cl (union F))) by XBOOLE_1:7;
hence (union F) \/ (Int (Cl (union F))) is condensed by A2, TOPS_1:def 6; :: thesis: verum