let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is domains-family holds
(meet F) /\ (Cl (Int (meet F))) is condensed
let F be Subset-Family of T; :: thesis: ( F is domains-family implies (meet F) /\ (Cl (Int (meet F))) is condensed )
A1: Int (Int (meet F)) c= Int (Cl (Int (meet F))) by PRE_TOPC:18, TOPS_1:19;
assume F is domains-family ; :: thesis: (meet F) /\ (Cl (Int (meet F))) is condensed
then Int (Cl (meet F)) c= meet F by Th66;
then A2: Int (Cl ((meet F) /\ (Cl (Int (meet F))))) c= (meet F) /\ (Cl (Int (meet F))) by Th6;
Cl (Int ((meet F) /\ (Cl (Int (meet F))))) = Cl ((Int (meet F)) /\ (Int (Cl (Int (meet F))))) by TOPS_1:17
.= Cl (Int (meet F)) by A1, XBOOLE_1:28 ;
then (meet F) /\ (Cl (Int (meet F))) c= Cl (Int ((meet F) /\ (Cl (Int (meet F))))) by XBOOLE_1:17;
hence (meet F) /\ (Cl (Int (meet F))) is condensed by A2, TOPS_1:def 6; :: thesis: verum