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 & ( 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;
A3: 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 A4: ( f in INTERSECTION {O},F & g in INTERSECTION {O},F ) ; :: thesis: ( f = g or f = {} or g = {} )
then consider o1, f1 being set such that
A5: ( o1 in {O} & f1 in F & f = o1 /\ f1 ) by SETFAM_1:def 5;
consider o2, g1 being set such that
A6: ( o2 in {O} & g1 in F & g = o2 /\ g1 ) by A4, SETFAM_1:def 5;
( {o1} c= {O} & {o2} c= {O} ) by A5, A6, ZFMISC_1:37;
then A7: ( o1 = O & o2 = O ) by ZFMISC_1:6;
then ( ( O meets f1 & O meets g1 ) or f = {} or g = {} ) by A5, A6, XBOOLE_0:def 7;
hence ( f = g or f = {} or g = {} ) by A2, A5, A6, A7; :: thesis: verum

end;

A8: 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 A9: ( 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 A3, A9;
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
A10: f in (INTERSECTION {O},F) \ {{} } by XBOOLE_0:def 1;
( f in INTERSECTION {O},F & f <> {} ) by A10, ZFMISC_1:64;
then A11: INTERSECTION {O},F c= {{} ,f} by A8;

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 A11, 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