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))
A1: Int (meet (Cl F)) c= meet (Int (Cl F)) by Th28;
Int (Cl (meet F)) c= Int (meet (Cl F)) by Th14, TOPS_1:19;
hence Int (Cl (meet F)) c= meet (Int (Cl F)) by A1; :: thesis: verum