let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is discrete holds
for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial )
let F be Subset-Family of T; :: thesis: ( F is discrete implies for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) )
assume A1: F is discrete ; :: thesis: for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial )
let p be Point of T; :: thesis: ex O being open Subset of T st
( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial )
consider O being open Subset of T such that
A2: p in O and
A3: 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;
set I = INTERSECTION ({O},F);
A4: for f, g being set st f in INTERSECTION ({O},F) & g in INTERSECTION ({O},F) & not f = g & not f = {} holds
g = {}

proof

let f, g be set ; :: thesis: ( f in INTERSECTION ({O},F) & g in INTERSECTION ({O},F) & not f = g & not f = {} implies g = {} )
assume that
A5: f in INTERSECTION ({O},F) and
A6: g in INTERSECTION ({O},F) ; :: thesis: ( f = g or f = {} or g = {} )
consider o1, f1 being set such that
A7: o1 in {O} and
A8: f1 in F and
A9: f = o1 /\ f1 by A5, SETFAM_1:def 5;
consider o2, g1 being set such that
A10: o2 in {O} and
A11: g1 in F and
A12: g = o2 /\ g1 by A6, SETFAM_1:def 5;
{o2} c= {O} by A10, ZFMISC_1:31;
then A13: o2 = O by ZFMISC_1:3;
{o1} c= {O} by A7, ZFMISC_1:31;
then A14: o1 = O by ZFMISC_1:3;
then ( ( O meets f1 & O meets g1 ) or f = {} or g = {} ) by A9, A12, A13, XBOOLE_0:def 7;
hence ( f = g or f = {} or g = {} ) by A3, A8, A9, A11, A12, A14, A13; :: thesis: verum

end;

A15: for f being set st f <> {} & f in INTERSECTION ({O},F) holds
INTERSECTION ({O},F) c= {{},f}

proof

let f be set ; :: thesis: ( f <> {} & f in INTERSECTION ({O},F) implies INTERSECTION ({O},F) c= {{},f} )
assume A16: ( f <> {} & f in INTERSECTION ({O},F) ) ; :: thesis: INTERSECTION ({O},F) c= {{},f}

now :: thesis: for g being object st g in INTERSECTION ({O},F) holds
g in {{},f}

let g be object ; :: thesis: ( g in INTERSECTION ({O},F) implies g in {{},f} )
assume g in INTERSECTION ({O},F) ; :: thesis: g in {{},f}
then ( f = g or g = {} ) by A4, A16;
hence g in {{},f} by TARSKI:def 2; :: thesis: verum

end;

hence INTERSECTION ({O},F) c= {{},f} ; :: thesis: verum

end;

now :: thesis: (INTERSECTION ({O},F)) \ {{}} is trivial

per cases ( (INTERSECTION ({O},F)) \ {{}} <> {} or (INTERSECTION ({O},F)) \ {{}} = {} ) ;

suppose (INTERSECTION ({O},F)) \ {{}} <> {} ; :: thesis: (INTERSECTION ({O},F)) \ {{}} is trivial

then consider f being object such that
A17: f in (INTERSECTION ({O},F)) \ {{}} by XBOOLE_0:def 1;
f <> {} by A17, ZFMISC_1:56;
then A18: INTERSECTION ({O},F) c= {{},f} by A15, A17;

now :: thesis: for g being object st g in INTERSECTION ({O},F) holds
g in {{}} \/ {f}

let g be object ; :: thesis: ( g in INTERSECTION ({O},F) implies g in {{}} \/ {f} )
assume g in INTERSECTION ({O},F) ; :: thesis: g in {{}} \/ {f}
then {g} c= {{},f} by A18, ZFMISC_1:31;
then ( g = {} or g = f ) by ZFMISC_1:19;
then ( g in {{}} or g in {f} ) by ZFMISC_1:31;
hence g in {{}} \/ {f} by XBOOLE_0:def 3; :: thesis: verum

end;

then INTERSECTION ({O},F) c= {{}} \/ {f} ;
then (INTERSECTION ({O},F)) \ {{}} c= {f} by XBOOLE_1:43;
then ( (INTERSECTION ({O},F)) \ {{}} = {} or (INTERSECTION ({O},F)) \ {{}} = {f} ) by ZFMISC_1:33;
hence (INTERSECTION ({O},F)) \ {{}} is trivial ; :: thesis: verum

end;

suppose (INTERSECTION ({O},F)) \ {{}} = {} ; :: thesis: (INTERSECTION ({O},F)) \ {{}} is trivial

hence (INTERSECTION ({O},F)) \ {{}} is trivial ; :: thesis: verum

end;

end;

end;

hence ex O being open Subset of T st
( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) by A2; :: thesis: verum