let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st F is discrete holds
F is locally_finite
let F be Subset-Family of T; :: thesis: ( F is discrete implies F is locally_finite )
assume A1: F is discrete ; :: thesis: F is locally_finite
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 )

proof

let p be Point of T; :: thesis: 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 )
consider U being open Subset of T such that
A2: ( p in U & ( 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, Def1;
take O = U; :: thesis: ( p in O & O is open & { D where D is Subset of T : ( D in F & D meets O ) } is finite )
set SF = { D where D is Subset of T : ( D in F & D meets U ) } ;
( { 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} )

proof

assume { D where D is Subset of T : ( D in F & D meets U ) } <> {} ; :: thesis: ex A being Subset of T st { D where D is Subset of T : ( D in F & D meets U ) } = {A}
then consider a being set such that
A3: 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
A4: ( a = D & D in F & D meets O ) by A3;

now

let b be set ; :: thesis: ( b in { D where D is Subset of T : ( D in F & D meets U ) } implies b in {D} )
assume b in { D where D is Subset of T : ( D in F & D meets U ) } ; :: thesis: b in {D}
then consider C being Subset of T such that
A5: ( b = C & C in F & C meets O ) ;
b = D by A2, A4, A5;
hence b in {D} by TARSKI:def 1; :: thesis: verum

end;

then ( { 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 A3, A4, TARSKI:def 3, ZFMISC_1:37;
then { D where D is Subset of T : ( D in F & D meets U ) } = {D} by 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: verum

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: verum

end;

hence F is locally_finite by PCOMPS_1:def 2; :: thesis: verum