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

proof

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;

hence Ball (t1,r) is bounded by Th10; :: thesis: verum