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 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: ( p in O & O is open & { D where D is Subset of T : ( D in F & D meets O ) } is finite )
( { 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 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;

now :: thesis: for b being object st b in { D where D is Subset of T : ( D in F & D meets U ) } holds
b in {D}

let b be object ; :: 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 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: verum

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