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 that
A1: F is discrete and
A2: G is discrete and
A3: INTERSECTION (F,G) = H ; :: thesis: H is discrete

now :: thesis: 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; :: 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
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 :: thesis: 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 = B

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 that
A9: A in INTERSECTION (F,G) and
A10: B in INTERSECTION (F,G) ; :: thesis: ( 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 ; :: thesis: A = B
consider 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; :: thesis: 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; :: thesis: verum

end;

hence H is discrete ; :: thesis: verum