let PM be MetrStruct ; :: thesis: for x being Element of PM ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )
let x be Element of PM; :: thesis: ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )
consider r being Real such that
A1: r = 1 ;
take r ; :: thesis: ( r > 0 & Ball (x,r) c= the carrier of PM )
thus r > 0 by A1; :: thesis: Ball (x,r) c= the carrier of PM
thus Ball (x,r) c= the carrier of PM ; :: thesis: verum