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