let T be TopSpace; :: thesis: for F being Subset-Family of T holds meet F c= meet (Cl F)
let F be Subset-Family of T; :: thesis: meet F c= meet (Cl F)
A1: for A being set st A in Cl F holds
meet F c= A

proof

let A be set ; :: thesis: ( A in Cl F implies meet F c= A )
assume A2: A in Cl F ; :: thesis: meet F c= A
then reconsider A0 = A as Subset of T ;
consider B being Subset of T such that
A3: A0 = Cl B and
A4: B in F by A2, PCOMPS_1:def 2;
A5: B c= A0 by A3, PRE_TOPC:18;
meet F c= B by A4, SETFAM_1:3;
hence meet F c= A by A5; :: thesis: verum

end;

now :: thesis: meet F c= meet (Cl F)

per cases ( Cl F = {} or Cl F <> {} ) ;

suppose Cl F = {} ; :: thesis: meet F c= meet (Cl F)

hence meet F c= meet (Cl F) by Th9; :: thesis: verum

end;

suppose Cl F <> {} ; :: thesis: meet F c= meet (Cl F)

hence meet F c= meet (Cl F) by A1, SETFAM_1:5; :: thesis: verum

end;

end;

end;

hence meet F c= meet (Cl F) ; :: thesis: verum