let T be TopSpace; :: thesis: for F, G being Subset-Family of T holds Cl (F /\ G) c= (Cl F) /\ (Cl G)
let F, G be Subset-Family of T; :: thesis: Cl (F /\ G) c= (Cl F) /\ (Cl G)
for X being set st X in Cl (F /\ G) holds
X in (Cl F) /\ (Cl G)

proof

let X be set ; :: thesis: ( X in Cl (F /\ G) implies X in (Cl F) /\ (Cl G) )
assume A1: X in Cl (F /\ G) ; :: thesis: X in (Cl F) /\ (Cl G)
then reconsider X0 = X as Subset of T ;
consider W being Subset of T such that
A2: X0 = Cl W and
A3: W in F /\ G by A1, PCOMPS_1:def 3;
A4: ( W in F & W in G ) by A3, XBOOLE_0:def 4;
then A5: X0 in Cl F by A2, PCOMPS_1:def 3;
X0 in Cl G by A2, A4, PCOMPS_1:def 3;
hence X in (Cl F) /\ (Cl G) by A5, XBOOLE_0:def 4; :: thesis: verum

end;

hence Cl (F /\ G) c= (Cl F) /\ (Cl G) by TARSKI:def 3; :: thesis: verum