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