let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: 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; :: thesis: for r being Real st 0 < r holds

Ball (t1,r) is bounded

let r be Real; :: thesis: ( 0 < r implies Ball (t1,r) is bounded )

assume A1: 0 < r ; :: thesis: 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 ) )

for r being Real st 0 < r holds

Ball (t1,r) is bounded

let t1 be Element of T; :: thesis: for r being Real st 0 < r holds

Ball (t1,r) is bounded

let r be Real; :: thesis: ( 0 < r implies Ball (t1,r) is bounded )

assume A1: 0 < r ; :: thesis: 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

hence
Ball (t1,r) is bounded
by Th10; :: thesis: verum
take
r
; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: for z being Point of T st z in Ball (t1,r) holds

dist (t1,z) <= r

let z be Point of T; :: thesis: ( z in Ball (t1,r) implies dist (t1,z) <= r )

assume z in Ball (t1,r) ; :: thesis: dist (t1,z) <= r

hence dist (t1,z) <= r by METRIC_1:11; :: thesis: verum

end;( 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 ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: for z being Point of T st z in Ball (t1,r) holds

dist (t1,z) <= r

let z be Point of T; :: thesis: ( z in Ball (t1,r) implies dist (t1,z) <= r )

assume z in Ball (t1,r) ; :: thesis: dist (t1,z) <= r

hence dist (t1,z) <= r by METRIC_1:11; :: thesis: verum