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