let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is domains-family holds
( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )
let F be Subset-Family of T; :: thesis: ( F is domains-family implies ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) )
assume A1: F is domains-family ; :: thesis: ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )

now :: thesis: for A being Subset of T st A in F holds
A c= Cl (Int A)

let A be Subset of T; :: thesis: ( A in F implies A c= Cl (Int A) )
reconsider B = A as Subset of T ;
assume A in F ; :: thesis: A c= Cl (Int A)
then B is condensed by A1;
hence A c= Cl (Int A) by TOPS_1:def 6; :: thesis: verum

end;

hence ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) by Th56; :: thesis: verum