let PM be MetrStruct ; for x being Element of PM
for r, p being Real st r <= p holds
Ball (x,r) c= Ball (x,p)
let x be Element of PM; for r, p being Real st r <= p holds
Ball (x,r) c= Ball (x,p)
let r, p be Real; ( r <= p implies Ball (x,r) c= Ball (x,p) )
assume A1:
r <= p
; Ball (x,r) c= Ball (x,p)
for y being Element of PM st y in Ball (x,r) holds
y in Ball (x,p)
hence
Ball (x,r) c= Ball (x,p)
; verum