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