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 )

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

hence
F is locally_finite
; :: thesis: verum
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} )

end;( 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

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
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;

{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;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}

then A7:
{ D where D is Subset of T : ( D in F & D meets U ) } c= {D}
;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;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

{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