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 ) ) )

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 ) ) )
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 )
proof
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 ;
set I = INTERSECTION ({O},F);
consider a being object such that
A12: ( (INTERSECTION ({O},F)) \ = {} or (INTERSECTION ({O},F)) \ = {a} ) by ;
A13: O in {O} by ZFMISC_1:31;
then O /\ B in INTERSECTION ({O},F) by ;
then O /\ B in (INTERSECTION ({O},F)) \ by ;
then {(O /\ B)} c= {a} by ;
then A14: O /\ B = a by ZFMISC_1:3;
A15: O /\ A <> {} by ;
then consider f being object such that
A16: f in O /\ A by XBOOLE_0:def 1;
A17: f in A by ;
O /\ A in INTERSECTION ({O},F) by ;
then O /\ A in (INTERSECTION ({O},F)) \ by ;
then {(O /\ A)} c= {a} by ;
then O /\ A = a by ZFMISC_1:3;
then f in B by ;
then A18: f in A /\ B by ;
A misses B by A2, A6, A7, A10;
hence contradiction by A18, XBOOLE_0:def 7; :: thesis: verum
end;
hence ( 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 ) ) ) by ; :: thesis: verum
end;
hence ( 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 ) ) ) ; :: thesis: verum