let T be non empty TopSpace; :: thesis: 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; :: thesis: ( F is discrete & G is discrete & INTERSECTION F,G = H implies H is discrete )
assume A1:
( F is discrete & G is discrete & INTERSECTION F,G = H )
; :: thesis: H is discrete
now let p be
Point of
T;
:: thesis: 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 A2:
(
p in O & ( 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, Def1;
consider U being
open Subset of
T such that A3:
(
p in U & ( for
A,
B being
Subset of
T st
A in G &
B in G &
U meets A &
U meets B holds
A = B ) )
by A1, Def1;
set Q =
O /\ U;
A4:
(
O /\ U is
open &
p in O /\ U )
by A2, A3, TOPS_1:38, XBOOLE_0:def 4;
now let A,
B be
Subset of
T;
:: thesis: ( A in INTERSECTION F,G & B in INTERSECTION F,G & O /\ U meets A & O /\ U meets B implies A = B )assume A5:
(
A in INTERSECTION F,
G &
B in INTERSECTION F,
G )
;
:: thesis: ( O /\ U meets A & O /\ U meets B implies A = B )then consider af,
ag being
set such that A6:
(
af in F &
ag in G &
A = af /\ ag )
by SETFAM_1:def 5;
consider bf,
bg being
set such that A7:
(
bf in F &
bg in G &
B = bf /\ bg )
by A5, SETFAM_1:def 5;
assume
(
O /\ U meets A &
O /\ U meets B )
;
:: thesis: A = Bthen
(
(O /\ U) /\ (af /\ ag) <> {} &
(O /\ U) /\ (bf /\ bg) <> {} )
by A6, A7, XBOOLE_0:def 7;
then
(
((O /\ U) /\ af) /\ ag <> {} &
((O /\ U) /\ bf) /\ bg <> {} )
by XBOOLE_1:16;
then
(
((O /\ af) /\ U) /\ ag <> {} &
((O /\ bf) /\ U) /\ bg <> {} )
by XBOOLE_1:16;
then
(
(O /\ af) /\ (U /\ ag) <> {} &
(O /\ bf) /\ (U /\ bg) <> {} )
by XBOOLE_1:16;
then
(
O /\ af <> {} &
U /\ ag <> {} &
O /\ bf <> {} &
U /\ bg <> {} )
;
then
(
O meets af &
O meets bf &
U meets ag &
U meets bg )
by XBOOLE_0:def 7;
then
(
af = bf &
ag = bg )
by A2, A3, A6, A7;
hence
A = B
by A6, A7;
:: thesis: verum end; 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 A1, A4;
:: thesis: verum end;
hence
H is discrete
by Def1; :: thesis: verum