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, Def1;
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:37;
then A13: o2 = O by ZFMISC_1:6;
{o1} c= {O} by A7, ZFMISC_1:37;
then A14: o1 = O by ZFMISC_1:6;
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

let g be set ; :: 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} by TARSKI:def 3; :: thesis: verum

end;

now

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

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

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

now

let g be set ; :: 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:37;
then ( g = {} or g = f ) by ZFMISC_1:25;
then ( g in {{} } or g in {f} ) by ZFMISC_1:37;
hence g in {{} } \/ {f} by XBOOLE_0:def 3; :: thesis: verum

end;

then INTERSECTION {O},F c= {{} } \/ {f} by TARSKI:def 3;
then (INTERSECTION {O},F) \ {{} } c= {f} by XBOOLE_1:43;
then ( (INTERSECTION {O},F) \ {{} } = {} or (INTERSECTION {O},F) \ {{} } = {f} ) by ZFMISC_1:39;
hence (INTERSECTION {O},F) \ {{} } is trivial by REALSET1:def 4; :: thesis: verum

end;

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

hence (INTERSECTION {O},F) \ {{} } is trivial by REALSET1:def 4; :: 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