let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F)))
let F be Subset-Family of T; :: thesis: Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F)))
Cl (Int (meet F)) c= meet (Cl (Int F)) by Th50;
then ( Int (meet (Cl (Int F))) c= meet (Int (Cl (Int F))) & Int (Cl (Int (meet F))) c= Int (meet (Cl (Int F))) ) by Th29, TOPS_1:48;
hence Int (Cl (Int (meet F))) c= meet (Int (Cl (Int F))) by XBOOLE_1:1; :: thesis: verum