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: