let T be non empty TopSpace; :: thesis:
let F be Subset-Family of T; :: thesis:
assume A1: F is discrete ; :: thesis:
for p being Point of T ex A being Subset of T st
( p in A & A is open & { D where D is Subset of T : ( D in F & D meets A ) } is finite )

let p be Point of T; :: thesis:
consider U being open Subset of T such that
A2: p in U and
A3: for A, B being Subset of T st A in F & B in F & U meets A & U meets B holds
A = B by A1;
set SF = { D where D is Subset of T : ( D in F & D meets U ) } ;
take O = U; :: thesis:
( { D where D is Subset of T : ( D in F & D meets U ) } <> {} implies ex A being Subset of T st { D where D is Subset of T : ( D in F & D meets U ) } = {A} )

assume { D where D is Subset of T : ( D in F & D meets U ) } <> {} ; :: thesis:
then consider a being object such that
A4: a in { D where D is Subset of T : ( D in F & D meets U ) } by XBOOLE_0:def 1;
consider D being Subset of T such that
A5: a = D and
A6: ( D in F & D meets O ) by A4;

let b be object ; :: thesis:
assume b in { D where D is Subset of T : ( D in F & D meets U ) } ; :: thesis:
then ex C being Subset of T st
( b = C & C in F & C meets O ) ;
then b = D by A3, A6;
hence b in {D} by TARSKI:def 1; :: thesis:

end;

then A7: { D where D is Subset of T : ( D in F & D meets U ) } c= {D} ;
{D} c= { D where D is Subset of T : ( D in F & D meets U ) } by A4, A5, ZFMISC_1:31;
then { D where D is Subset of T : ( D in F & D meets U ) } = {D} by A7, XBOOLE_0:def 10;
hence ex A being Subset of T st { D where D is Subset of T : ( D in F & D meets U ) } = {A} ; :: thesis:

end;

hence ( p in O & O is open & { D where D is Subset of T : ( D in F & D meets O ) } is finite ) by A2; :: thesis:

end;