let X be RealUnitarySpace; :: thesis: for y, x being Point of X
for r, q being Real st y in Ball (x,r) & r <= q holds
y in Ball (x,q)
let y, x be Point of X; :: thesis: for r, q being Real st y in Ball (x,r) & r <= q holds
y in Ball (x,q)
let r, q 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