let T be non empty TopSpace; :: thesis: for F being Subset-Family of T

for A, B being Subset of T st F is discrete & A in F & B in F & not A = B holds

A misses B

let F be Subset-Family of T; :: thesis: for A, B being Subset of T st F is discrete & A in F & B in F & not A = B holds

A misses B

let A, B be Subset of T; :: thesis: ( F is discrete & A in F & B in F & not A = B implies A misses B )

assume that

A1: F is discrete and

A2: ( A in F & B in F ) ; :: thesis: ( A = B or A misses B )

assume that

A3: A <> B and

A4: A meets B ; :: thesis: contradiction

A /\ B <> {} T by A4, XBOOLE_0:def 7;

then consider p being Point of T such that

A5: p in A /\ B by PRE_TOPC:12;

consider O being open Subset of T such that

A6: p in O and

A7: for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D by A1;

A8: {p} c= O by A6, ZFMISC_1:31;

p in B by A5, XBOOLE_0:def 4;

then {p} c= B by ZFMISC_1:31;

then {p} c= O /\ B by A8, XBOOLE_1:19;

then A9: p in O /\ B by ZFMISC_1:31;

p in A by A5, XBOOLE_0:def 4;

then {p} c= A by ZFMISC_1:31;

then {p} c= O /\ A by A8, XBOOLE_1:19;

then A10: p in O /\ A by ZFMISC_1:31;

( O meets A & O meets B implies A = B ) by A2, A7;

hence contradiction by A3, A10, A9, XBOOLE_0:4; :: thesis: verum

for A, B being Subset of T st F is discrete & A in F & B in F & not A = B holds

A misses B

let F be Subset-Family of T; :: thesis: for A, B being Subset of T st F is discrete & A in F & B in F & not A = B holds

A misses B

let A, B be Subset of T; :: thesis: ( F is discrete & A in F & B in F & not A = B implies A misses B )

assume that

A1: F is discrete and

A2: ( A in F & B in F ) ; :: thesis: ( A = B or A misses B )

assume that

A3: A <> B and

A4: A meets B ; :: thesis: contradiction

A /\ B <> {} T by A4, XBOOLE_0:def 7;

then consider p being Point of T such that

A5: p in A /\ B by PRE_TOPC:12;

consider O being open Subset of T such that

A6: p in O and

A7: for C, D being Subset of T st C in F & D in F & O meets C & O meets D holds

C = D by A1;

A8: {p} c= O by A6, ZFMISC_1:31;

p in B by A5, XBOOLE_0:def 4;

then {p} c= B by ZFMISC_1:31;

then {p} c= O /\ B by A8, XBOOLE_1:19;

then A9: p in O /\ B by ZFMISC_1:31;

p in A by A5, XBOOLE_0:def 4;

then {p} c= A by ZFMISC_1:31;

then {p} c= O /\ A by A8, XBOOLE_1:19;

then A10: p in O /\ A by ZFMISC_1:31;

( O meets A & O meets B implies A = B ) by A2, A7;

hence contradiction by A3, A10, A9, XBOOLE_0:4; :: thesis: verum