let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is open-domains-family holds
( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed )
let F be Subset-Family of T; :: thesis: ( F is open-domains-family implies ( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed ) )
assume F is open-domains-family ; :: thesis: ( Int (meet F) is open_condensed & Int (Cl (union F)) is open_condensed )
then F is domains-family by Th79;
then Int (Cl (Int (meet F))) = Int (meet F) by Th66;
hence Int (meet F) is open_condensed by TOPS_1:def 8; :: thesis: Int (Cl (union F)) is open_condensed
thus Int (Cl (union F)) is open_condensed by TDLAT_1:23; :: thesis: verum