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 A1: ( F is discrete & A in F & B in F ) ; :: thesis: ( A = B or A misses B )
assume A2: ( A <> B & A meets B ) ; :: thesis: contradiction
then A /\ B <> {} T by XBOOLE_0:def 7;
then consider p being Point of T such that
A3: p in A /\ B by PRE_TOPC:41;
A4: ( p in A & p in B ) by A3, XBOOLE_0:def 4;
consider O being open Subset of T such that
A5: ( p in O & ( 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, Def1;
A6: ( O meets A & O meets B implies A = B ) by A1, A5;
( {p} c= A & {p} c= B & {p} c= O ) by A4, A5, ZFMISC_1:37;
then ( {p} c= O /\ A & {p} c= O /\ B ) by XBOOLE_1:19;
then ( p in O /\ A & p in O /\ B ) by ZFMISC_1:37;
hence contradiction by A2, A6, XBOOLE_0:4; :: thesis: verum