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 )
assume F is domains-family ; :: thesis: (meet F) /\ (Cl (Int (meet F))) is condensed
then A1: Int (Cl (meet F)) c= meet F by Th67;
A2: Int (Int (meet F)) c= Int (Cl (Int (meet F))) by PRE_TOPC:48, TOPS_1:48;
A3: (meet F) /\ (Cl (Int (meet F))) c= Cl (Int ((meet F) /\ (Cl (Int (meet F)))))

proof

Cl (Int ((meet F) /\ (Cl (Int (meet F))))) = Cl ((Int (meet F)) /\ (Int (Cl (Int (meet F))))) by TOPS_1:46
.= Cl (Int (meet F)) by A2, XBOOLE_1:28 ;
hence (meet F) /\ (Cl (Int (meet F))) c= Cl (Int ((meet F) /\ (Cl (Int (meet F))))) by XBOOLE_1:17; :: thesis: verum

end;

Int (Cl ((meet F) /\ (Cl (Int (meet F))))) c= (meet F) /\ (Cl (Int (meet F))) by A1, Th6;
hence (meet F) /\ (Cl (Int (meet F))) is condensed by A3, TOPS_1:def 6; :: thesis: verum