let X be RealUnitarySpace; :: thesis: for x, y being Point of X

for q, r being Real st y in Ball (x,r) & r <= q holds

y in Ball (x,q)

let x, y be Point of X; :: thesis: for q, r being Real st y in Ball (x,r) & r <= q holds

y in Ball (x,q)

let q, r be Real; :: thesis: ( y in Ball (x,r) & r <= q implies y in Ball (x,q) )

assume that

A1: y in Ball (x,r) and

A2: r <= q ; :: thesis: y in Ball (x,q)

||.(x - y).|| < r by A1, Th40;

then ||.(x - y).|| < q by A2, XXREAL_0:2;

hence y in Ball (x,q) ; :: thesis: verum

for q, r being Real st y in Ball (x,r) & r <= q holds

y in Ball (x,q)

let x, y be Point of X; :: thesis: for q, r being Real st y in Ball (x,r) & r <= q holds

y in Ball (x,q)

let q, r be Real; :: thesis: ( y in Ball (x,r) & r <= q implies y in Ball (x,q) )

assume that

A1: y in Ball (x,r) and

A2: r <= q ; :: thesis: y in Ball (x,q)

||.(x - y).|| < r by A1, Th40;

then ||.(x - y).|| < q by A2, XXREAL_0:2;

hence y in Ball (x,q) ; :: thesis: verum