let r, s be Real; :: thesis: for n being Element of NAT
for x being Point of (TOP-REAL n) st r <= s holds
Ball (x,r) c= Ball (x,s)
let n be Element of NAT ; :: thesis: for x being Point of (TOP-REAL n) st r <= s holds
Ball (x,r) c= Ball (x,s)
let x be Point of (TOP-REAL n); :: thesis: ( r <= s implies Ball (x,r) c= Ball (x,s) )
reconsider xe = x as Point of (Euclid n) by TOPREAL3:8;
A1: Ball (x,r) = Ball (xe,r) by TOPREAL9:13;
Ball (x,s) = Ball (xe,s) by TOPREAL9:13;
hence ( r <= s implies Ball (x,r) c= Ball (x,s) ) by A1, PCOMPS_1:1; :: thesis: verum