let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is domains-family holds
( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
let F be Subset-Family of T; :: thesis: ( F is domains-family implies ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) )
assume A1: F is domains-family ; :: thesis: ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) )
now :: thesis: for A being Subset of T st A in F holds
Int (Cl A) c= A
let A be Subset of T; :: thesis: ( A in F implies Int (Cl A) c= A )
reconsider B = A as Subset of T ;
assume A in F ; :: thesis: Int (Cl A) c= A
then B is condensed by A1;
hence Int (Cl A) c= A by TOPS_1:def 6; :: thesis: verum
end;
hence ( Int (Cl (meet F)) c= meet F & Int (Cl (Int (meet F))) = Int (meet F) ) by Th57; :: thesis: verum