let p be Point of (TOP-REAL 2); :: thesis: for e being Point of (Euclid 2)
for D being non empty Subset of (TOP-REAL 2)
for r being Real st D = Ball (e,r) & p = e holds
E-bound D = (p `1) + r
let e be Point of (Euclid 2); :: thesis: for D being non empty Subset of (TOP-REAL 2)
for r being Real st D = Ball (e,r) & p = e holds
E-bound D = (p `1) + r
let D be non empty Subset of (TOP-REAL 2); :: thesis: for r being Real st D = Ball (e,r) & p = e holds
E-bound D = (p `1) + r
let r be Real; :: thesis: ( D = Ball (e,r) & p = e implies E-bound D = (p `1) + r )
assume that
A1: D = Ball (e,r) and
A2: p = e ; :: thesis: E-bound D = (p `1) + r
r > 0 by A1, TBSP_1:12;
then A3: (p `1) + 0 < (p `1) + r by XREAL_1:6;
(p `1) - r < (p `1) - 0 by A1, TBSP_1:12, XREAL_1:15;
then (p `1) - r < (p `1) + r by A3, XXREAL_0:2;
then A4: upper_bound ].((p `1) - r),((p `1) + r).[ = (p `1) + r by Th16;
proj1 .: D = ].((p `1) - r),((p `1) + r).[ by A1, A2, Th41;
hence E-bound D = (p `1) + r by A4, SPRECT_1:46; :: thesis: verum