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