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