let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is domains-family holds
Int F is open-domains-family
let F be Subset-Family of T; :: thesis: ( F is domains-family implies Int F is open-domains-family )
assume A1: F is domains-family ; :: thesis: Int F is open-domains-family
for A being Subset of T st A in Int F holds
A is open_condensed

proof

let A be Subset of T; :: thesis: ( A in Int F implies A is open_condensed )
assume A in Int F ; :: thesis: A is open_condensed
then consider P being Subset of T such that
A2: A = Int P and
A3: P in F by Def1;
reconsider P = P as Subset of T ;
P is condensed by A1, A3;
hence A is open_condensed by A2, TDLAT_1:25; :: thesis: verum

end;

hence Int F is open-domains-family ; :: thesis: verum