let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is closed-domains-family holds
( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed )
let F be Subset-Family of T; :: thesis: ( F is closed-domains-family implies ( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed ) )
assume F is closed-domains-family ; :: thesis: ( Cl (union F) is closed_condensed & Cl (Int (meet F)) is closed_condensed )
then F is domains-family by Th72;
then Cl (union F) = Cl (Int (Cl (union F))) by Th65;
hence Cl (union F) is closed_condensed by TOPS_1:def 7; :: thesis: Cl (Int (meet F)) is closed_condensed
thus Cl (Int (meet F)) is closed_condensed by TDLAT_1:22; :: thesis: verum