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

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

hence
H is discrete
; :: thesis: verum( 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;

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;( 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

set Q = O /\ U;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;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

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