let T be non empty TopSpace; for F, G, H being Subset-Family of T st F is discrete & G is discrete & INTERSECTION (F,G) = H holds
H is discrete
let F, G, H be Subset-Family of T; ( F is discrete & G is discrete & INTERSECTION (F,G) = H implies H is discrete )
assume that
A1:
F is discrete
and
A2:
G is discrete
and
A3:
INTERSECTION (F,G) = H
; H is discrete
now for p being Point of T ex Q being open Subset of T st
( p in Q & ( for A, B being Subset of T st A in H & B in H & Q meets A & Q meets B holds
A = B ) )let p be
Point of
T;
ex Q being open Subset of T st
( p in Q & ( for A, B being Subset of T st A in H & B in H & Q meets A & Q meets B holds
A = B ) )consider O being
open Subset of
T such that A4:
p in O
and A5:
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;
consider U being
open Subset of
T such that A6:
p in U
and A7:
for
A,
B being
Subset of
T st
A in G &
B in G &
U meets A &
U meets B holds
A = B
by A2;
A8:
now for A, B being Subset of T st A in INTERSECTION (F,G) & B in INTERSECTION (F,G) & O /\ U meets A & O /\ U meets B holds
A = Blet A,
B be
Subset of
T;
( A in INTERSECTION (F,G) & B in INTERSECTION (F,G) & O /\ U meets A & O /\ U meets B implies A = B )assume that A9:
A in INTERSECTION (
F,
G)
and A10:
B in INTERSECTION (
F,
G)
;
( O /\ U meets A & O /\ U meets B implies A = B )consider af,
ag being
set such that A11:
af in F
and A12:
ag in G
and A13:
A = af /\ ag
by A9, SETFAM_1:def 5;
assume that A14:
O /\ U meets A
and A15:
O /\ U meets B
;
A = Bconsider bf,
bg being
set such that A16:
bf in F
and A17:
bg in G
and A18:
B = bf /\ bg
by A10, SETFAM_1:def 5;
(O /\ U) /\ (bf /\ bg) <> {}
by A18, A15, XBOOLE_0:def 7;
then
((O /\ U) /\ bf) /\ bg <> {}
by XBOOLE_1:16;
then A19:
((O /\ bf) /\ U) /\ bg <> {}
by XBOOLE_1:16;
then
O /\ bf <> {}
;
then A20:
O meets bf
by XBOOLE_0:def 7;
(O /\ U) /\ (af /\ ag) <> {}
by A13, A14, XBOOLE_0:def 7;
then
((O /\ U) /\ af) /\ ag <> {}
by XBOOLE_1:16;
then A21:
((O /\ af) /\ U) /\ ag <> {}
by XBOOLE_1:16;
then
(O /\ af) /\ (U /\ ag) <> {}
by XBOOLE_1:16;
then
U /\ ag <> {}
;
then A22:
U meets ag
by XBOOLE_0:def 7;
(O /\ bf) /\ (U /\ bg) <> {}
by A19, XBOOLE_1:16;
then
U /\ bg <> {}
;
then A23:
U meets bg
by XBOOLE_0:def 7;
O /\ af <> {}
by A21;
then
O meets af
by XBOOLE_0:def 7;
then
af = bf
by A5, A11, A16, A20;
hence
A = B
by A7, A12, A13, A17, A18, A22, A23;
verum end; set Q =
O /\ U;
p in O /\ U
by A4, A6, XBOOLE_0:def 4;
hence
ex
Q being
open Subset of
T st
(
p in Q & ( for
A,
B being
Subset of
T st
A in H &
B in H &
Q meets A &
Q meets B holds
A = B ) )
by A3, A8;
verum end;
hence
H is discrete
; verum