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