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)
Cl F is closed by PCOMPS_1:14;
then ( meet (Cl F) is closed & meet F c= meet (Cl F) ) by Th13, TOPS_2:29;
then ( Cl (meet (Cl F)) = meet (Cl F) & Cl (meet F) c= Cl (meet (Cl F)) ) by PRE_TOPC:49, PRE_TOPC:52;
hence Cl (meet F) c= meet (Cl F) ; :: thesis: verum