let T be TopSpace; :: thesis: for F being Subset-Family of T holds Cl (meet F) c= meet (Cl F)
let F be Subset-Family of T; :: thesis: Cl (meet F) c= meet (Cl F)
A1: meet (Cl F) is closed by PCOMPS_1:11, TOPS_2:22;
Cl (meet F) c= Cl (meet (Cl F)) by Th13, PRE_TOPC:19;
hence Cl (meet F) c= meet (Cl F) by A1, PRE_TOPC:22; :: thesis: verum