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
A3: r / 2 > 0 by A1, XREAL_1:215;
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 A4: 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 1 :: 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 x9 = x as Point of M ;
reconsider B = Ball (x9,(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 )
A5: dist (x9,x9) = 0 by METRIC_1:1;
B in Family_open_set M by PCOMPS_1:29;
hence ( x in B & B is open ) by A5, A3, METRIC_1:11, PRE_TOPC:def 2; :: 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,x9) >= r / 2 or ex p being Point of M st
( p in A & dist (p,x9) < r / 2 ) ) ;

suppose A6: for p being Point of M st p in A holds
dist (p,x9) >= 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 object such that
A7: 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
v = V and
A8: V in F and
A9: V meets B by A7;
consider y being Point of (TopSpaceMetr M) such that
A10: V = {y} and
A11: y in A by A4, A8;
reconsider y = y as Point of M ;
y in B by A9, A10, ZFMISC_1:50;
then dist (x9,y) < r / 2 by METRIC_1:11;
hence contradiction by A6, 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;

suppose ex p being Point of M st
( p in A & dist (p,x9) < 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
A12: p in A and
A13: dist (p,x9) < r / 2 ;
{ V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } c= {{p}}

proof

let v be object ; :: 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 v in { V where V is Subset of (TopSpaceMetr M) : ( V in F & V meets B ) } ; :: thesis: v in {{p}}
then consider V being Subset of (TopSpaceMetr M) such that
A14: v = V and
A15: V in F and
A16: V meets B ;
consider y being Point of (TopSpaceMetr M) such that
A17: V = {y} and
A18: y in A by A4, A15;
reconsider y = y as Point of M ;
y in B by A16, A17, ZFMISC_1:50;
then dist (x9,y) < r / 2 by METRIC_1:11;
then A19: (dist (p,x9)) + (dist (x9,y)) < (r / 2) + (r / 2) by A13, XREAL_1:8;
dist (p,y) <= (dist (p,x9)) + (dist (x9,y)) by METRIC_1:4;
then dist (p,y) < (r / 2) + (r / 2) by A19, XXREAL_0:2;
then p = y by A2, A12, A18;
hence v in {{p}} by A14, A17, TARSKI:def 1; :: 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;