let T be non empty TopSpace; 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; 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; ( 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 )
; ( A = B or A misses B )
assume that
A3:
A <> B
and
A4:
A meets B
; 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; verum