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 object st X in Cl (F /\ G) holds
X in (Cl F) /\ (Cl G)

proof

let X be object ; :: 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 2;
W in G by A3, XBOOLE_0:def 4;
then A4: X0 in Cl G by A2, PCOMPS_1:def 2;
W in F by A3, XBOOLE_0:def 4;
then X0 in Cl F by A2, PCOMPS_1:def 2;
hence X in (Cl F) /\ (Cl G) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

hence Cl (F /\ G) c= (Cl F) /\ (Cl G) ; :: thesis: verum