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