let T be non empty Reflexive symmetric triangle MetrStruct ; for t1 being Element of T
for r being Real st 0 < r holds
Ball (t1,r) is bounded
let t1 be Element of T; for r being Real st 0 < r holds
Ball (t1,r) is bounded
let r be Real; ( 0 < r implies Ball (t1,r) is bounded )
assume A1:
0 < r
; Ball (t1,r) is bounded
set P = Ball (t1,r);
reconsider r = r as Real ;
ex r being Real ex t1 being Element of T st
( 0 < r & t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r ) )
proof
take
r
;
ex t1 being Element of T st
( 0 < r & t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r ) )
take
t1
;
( 0 < r & t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r ) )
thus
0 < r
by A1;
( t1 in Ball (t1,r) & ( for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r ) )
thus
t1 in Ball (
t1,
r)
by A1, Th11;
for z being Point of T st z in Ball (t1,r) holds
dist (t1,z) <= r
let z be
Point of
T;
( z in Ball (t1,r) implies dist (t1,z) <= r )
assume
z in Ball (
t1,
r)
;
dist (t1,z) <= r
hence
dist (
t1,
z)
<= r
by METRIC_1:11;
verum
end;
hence
Ball (t1,r) is bounded
by Th10; verum