let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for r being Real
for A being Subset of M st r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist p,q >= r ) holds
for F being Subset-Family of (TopSpaceMetr M) st F = { {x} where x is Element of (TopSpaceMetr M) : x in A } holds
F is locally_finite
set T = TopSpaceMetr M;
let r be Real; :: thesis: for A being Subset of M st r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist p,q >= r ) holds
for F being Subset-Family of (TopSpaceMetr M) st F = { {x} where x is Element of (TopSpaceMetr M) : x in A } holds
F is locally_finite
let A be Subset of M; :: thesis: ( r > 0 & ( for p, q being Point of M st p <> q & p in A & q in A holds
dist p,q >= r ) implies for F being Subset-Family of (TopSpaceMetr M) st F = { {x} where x is Element of (TopSpaceMetr M) : x in A } holds
F is locally_finite )
assume that
A1: r > 0 and
A2: for p, q being Point of M st p <> q & p in A & q in A holds
dist p,q >= r ; :: thesis: for F being Subset-Family of (TopSpaceMetr M) st F = { {x} where x is Element of (TopSpaceMetr M) : x in A } holds
F is locally_finite
let F be Subset-Family of (TopSpaceMetr M); :: thesis: ( F = { {x} where x is Element of (TopSpaceMetr M) : x in A } implies F is locally_finite )
assume A3: F = { {x} where x is Element of (TopSpaceMetr M) : x in A } ; :: thesis: F is locally_finite
let x be Point of (TopSpaceMetr M); :: according to PCOMPS_1:def 2 :: thesis: ex b₁ being Element of bool the carrier of (TopSpaceMetr M) st
( x in b₁ & b₁ is open & { b₂ where b₂ is Element of bool the carrier of (TopSpaceMetr M) : ( b₂ in F & not b₂ misses b₁ ) } is finite )
reconsider x' = x as Point of M ;
reconsider B = Ball x',(r / 2) as Subset of (TopSpaceMetr M) ;
take B ; :: thesis: ( x in B & B is open & { b₁ where b₁ is Element of bool the carrier of (TopSpaceMetr M) : ( b₁ in F & not b₁ misses B ) } is finite )
( B in Family_open_set M & dist x',x' = 0 & r / 2 > 0 ) by A1, METRIC_1:1, PCOMPS_1:33, XREAL_1:217;
hence ( x in B & B is open ) by METRIC_1:12, PRE_TOPC:def 5; :: thesis: { b₁ where b₁ is Element of bool the carrier of (TopSpaceMetr M) : ( b₁ in F & not b₁ misses B ) } is finite
set VV = { V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } ;

per cases ( for p being Point of M st p in A holds
dist p,x' >= r / 2 or ex p being Point of M st
( p in A & dist p,x' < r / 2 ) ) ;

suppose A4: for p being Point of M st p in A holds
dist p,x' >= r / 2 ; :: thesis: { b₁ where b₁ is Element of bool the carrier of (TopSpaceMetr M) : ( b₁ in F & not b₁ misses B ) } is finite

{ V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } is empty

proof

assume not { V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } is empty ; :: thesis: contradiction
then consider v being set such that
A5: v in { V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } by XBOOLE_0:def 1;
consider V being Subset of (TopSpaceMetr M) such that
A6: ( v = V & V in F & V meets B ) by A5;
consider y being Point of (TopSpaceMetr M) such that
A7: ( V = {y} & y in A ) by A3, A6;
reconsider y = y as Point of M ;
y in B by A6, A7, ZFMISC_1:56;
then dist x',y < r / 2 by METRIC_1:12;
hence contradiction by A4, A7; :: thesis: verum

end;

hence { b₁ where b₁ is Element of bool the carrier of (TopSpaceMetr M) : ( b₁ in F & not b₁ misses B ) } is finite ; :: thesis: verum

end;

suppose ex p being Point of M st
( p in A & dist p,x' < r / 2 ) ; :: thesis: { b₁ where b₁ is Element of bool the carrier of (TopSpaceMetr M) : ( b₁ in F & not b₁ misses B ) } is finite

then consider p being Point of M such that
A8: ( p in A & dist p,x' < r / 2 ) ;
{ V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } c= {{p}}

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in { V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } or v in {{p}} )
assume A9: v in { V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } ; :: thesis: v in {{p}}
consider V being Subset of (TopSpaceMetr M) such that
A10: ( v = V & V in F & V meets B ) by A9;
consider y being Point of (TopSpaceMetr M) such that
A11: ( V = {y} & y in A ) by A3, A10;
reconsider y = y as Point of M ;
y in B by A10, A11, ZFMISC_1:56;
then dist x',y < r / 2 by METRIC_1:12;
then ( dist p,y <= (dist p,x') + (dist x',y) & (dist p,x') + (dist x',y) < (r / 2) + (r / 2) ) by A8, METRIC_1:4, XREAL_1:10;
then dist p,y < (r / 2) + (r / 2) by XXREAL_0:2;
then ( p = y & {p} in {{p}} ) by A2, A8, A11, TARSKI:def 1;
hence v in {{p}} by A10, A11; :: thesis: verum

end;

hence { b₁ where b₁ is Element of bool the carrier of (TopSpaceMetr M) : ( b₁ in F & not b₁ misses B ) } is finite ; :: thesis: verum

end;

end;