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

( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) )

let F be Subset-Family of T; :: thesis: ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) )

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) ) ; :: thesis: verum

( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) )

let F be Subset-Family of T; :: thesis: ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) )

now :: thesis: for F being Subset-Family of T holds

( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) )

hence
( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) )

let F be Subset-Family of T; :: thesis: ( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) )

( ( for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) implies F is discrete )

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) ) by Th6, Th7; :: thesis: verum

end;( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) )

( ( for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) implies F is discrete )

proof

hence
( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st
assume that

A1: for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) and

A2: for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ; :: thesis: F is discrete

assume not F is discrete ; :: thesis: contradiction

then consider p being Point of T such that

A3: for O being open Subset of T holds

( not p in O or ex A, B being Subset of T st

( A in F & B in F & O meets A & O meets B & not A = B ) ) ;

consider O being open Subset of T such that

A4: p in O and

A5: (INTERSECTION ({O},F)) \ {{}} is trivial by A1;

consider A, B being Subset of T such that

A6: A in F and

A7: B in F and

A8: O meets A and

A9: O meets B and

A10: A <> B by A3, A4;

A11: O /\ B <> {} by A9, XBOOLE_0:def 7;

set I = INTERSECTION ({O},F);

consider a being object such that

A12: ( (INTERSECTION ({O},F)) \ {{}} = {} or (INTERSECTION ({O},F)) \ {{}} = {a} ) by A5, ZFMISC_1:131;

A13: O in {O} by ZFMISC_1:31;

then O /\ B in INTERSECTION ({O},F) by A7, SETFAM_1:def 5;

then O /\ B in (INTERSECTION ({O},F)) \ {{}} by A11, ZFMISC_1:56;

then {(O /\ B)} c= {a} by A12, ZFMISC_1:31;

then A14: O /\ B = a by ZFMISC_1:3;

A15: O /\ A <> {} by A8, XBOOLE_0:def 7;

then consider f being object such that

A16: f in O /\ A by XBOOLE_0:def 1;

A17: f in A by A16, XBOOLE_0:def 4;

O /\ A in INTERSECTION ({O},F) by A6, A13, SETFAM_1:def 5;

then O /\ A in (INTERSECTION ({O},F)) \ {{}} by A15, ZFMISC_1:56;

then {(O /\ A)} c= {a} by A12, ZFMISC_1:31;

then O /\ A = a by ZFMISC_1:3;

then f in B by A14, A16, XBOOLE_0:def 4;

then A18: f in A /\ B by A17, XBOOLE_0:def 4;

A misses B by A2, A6, A7, A10;

hence contradiction by A18, XBOOLE_0:def 7; :: thesis: verum

end;A1: for p being Point of T ex O being open Subset of T st

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) and

A2: for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ; :: thesis: F is discrete

assume not F is discrete ; :: thesis: contradiction

then consider p being Point of T such that

A3: for O being open Subset of T holds

( not p in O or ex A, B being Subset of T st

( A in F & B in F & O meets A & O meets B & not A = B ) ) ;

consider O being open Subset of T such that

A4: p in O and

A5: (INTERSECTION ({O},F)) \ {{}} is trivial by A1;

consider A, B being Subset of T such that

A6: A in F and

A7: B in F and

A8: O meets A and

A9: O meets B and

A10: A <> B by A3, A4;

A11: O /\ B <> {} by A9, XBOOLE_0:def 7;

set I = INTERSECTION ({O},F);

consider a being object such that

A12: ( (INTERSECTION ({O},F)) \ {{}} = {} or (INTERSECTION ({O},F)) \ {{}} = {a} ) by A5, ZFMISC_1:131;

A13: O in {O} by ZFMISC_1:31;

then O /\ B in INTERSECTION ({O},F) by A7, SETFAM_1:def 5;

then O /\ B in (INTERSECTION ({O},F)) \ {{}} by A11, ZFMISC_1:56;

then {(O /\ B)} c= {a} by A12, ZFMISC_1:31;

then A14: O /\ B = a by ZFMISC_1:3;

A15: O /\ A <> {} by A8, XBOOLE_0:def 7;

then consider f being object such that

A16: f in O /\ A by XBOOLE_0:def 1;

A17: f in A by A16, XBOOLE_0:def 4;

O /\ A in INTERSECTION ({O},F) by A6, A13, SETFAM_1:def 5;

then O /\ A in (INTERSECTION ({O},F)) \ {{}} by A15, ZFMISC_1:56;

then {(O /\ A)} c= {a} by A12, ZFMISC_1:31;

then O /\ A = a by ZFMISC_1:3;

then f in B by A14, A16, XBOOLE_0:def 4;

then A18: f in A /\ B by A17, XBOOLE_0:def 4;

A misses B by A2, A6, A7, A10;

hence contradiction by A18, XBOOLE_0:def 7; :: thesis: verum

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) ) by Th6, Th7; :: thesis: verum

( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds

A misses B ) ) ) ; :: thesis: verum