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)

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)end;

hence
Cl (A /\ B) = (Cl A) /\ (Cl B)
; :: thesis: verumper cases
( A misses B or A = B )
by A1, A2, Th6;

end;

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) = {}

end;(Cl A) /\ (Cl B) = {}

proof

hence
Cl (A /\ B) = (Cl A) /\ (Cl B)
by A3, PRE_TOPC:22; :: thesis: verum
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;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