let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis:
let t1 be Element of T; :: thesis:
let r be real number ; :: thesis:
assume A1: 0 < r ; :: thesis:
set P = Ball (t1,r);
reconsider r = r as Real by XREAL_0:def 1;
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:
take t1 ; :: thesis:
thus 0 < r by A1; :: thesis:
thus t1 in Ball (t1,r) by A1, Th16; :: thesis:
let z be Point of T; :: thesis:
assume z in Ball (t1,r) ; :: thesis:
hence dist (t1,z) <= r by METRIC_1:12; :: thesis:

end;

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