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