let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is discrete holds
for A, B being Subset of T st A in F & B in F holds
Cl (A /\ B) = (Cl A) /\ (Cl B)
let F be Subset-Family of T; :: thesis: ( F is discrete implies for A, B being Subset of T st A in F & B in F holds
Cl (A /\ B) = (Cl A) /\ (Cl B) )
assume A1: F is discrete ; :: thesis: for A, B being Subset of T st A in F & B in F holds
Cl (A /\ B) = (Cl A) /\ (Cl B)
let A, B be Subset of T; :: thesis: ( A in F & B in F implies Cl (A /\ B) = (Cl A) /\ (Cl B) )
assume A2: ( A in F & B in F ) ; :: thesis: Cl (A /\ B) = (Cl A) /\ (Cl B)

now :: thesis: Cl (A /\ B) = (Cl A) /\ (Cl B)

per cases ( A misses B or A = B ) by A1, A2, Th6;

suppose A misses B ; :: thesis: Cl (A /\ B) = (Cl A) /\ (Cl B)

then A3: A /\ B = {} T by XBOOLE_0:def 7;
(Cl A) /\ (Cl B) = {}

proof

assume (Cl A) /\ (Cl B) <> {} ; :: thesis: contradiction
then consider x being object such that
A4: x in (Cl A) /\ (Cl B) by XBOOLE_0:def 1;
consider O being open Subset of T such that
A5: x in O and
A6: for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B by A1, A4;
x in Cl A by A4, XBOOLE_0:def 4;
then A7: O meets A by A5, PRE_TOPC:def 7;
x in Cl B by A4, XBOOLE_0:def 4;
then O meets B by A5, PRE_TOPC:def 7;
then A = B by A2, A6, A7;
hence contradiction by A3, A7, XBOOLE_1:65; :: thesis: verum

end;

hence Cl (A /\ B) = (Cl A) /\ (Cl B) by A3, PRE_TOPC:22; :: thesis: verum

end;

suppose A = B ; :: thesis: Cl (A /\ B) = (Cl A) /\ (Cl B)

hence Cl (A /\ B) = (Cl A) /\ (Cl B) ; :: thesis: verum

end;

end;

end;

hence Cl (A /\ B) = (Cl A) /\ (Cl B) ; :: thesis: verum