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 number st D = Ball e,r & p = e holds
S-bound D = (p `2 ) - r
let e be Point of (Euclid 2); :: thesis: for D being non empty Subset of (TOP-REAL 2)
for r being real number st D = Ball e,r & p = e holds
S-bound D = (p `2 ) - r
let D be non empty Subset of (TOP-REAL 2); :: thesis: for r being real number st D = Ball e,r & p = e holds
S-bound D = (p `2 ) - r
let r be real number ; :: thesis: ( D = Ball e,r & p = e implies S-bound D = (p `2 ) - r )
assume that
A1: D = Ball e,r and
A2: p = e ; :: thesis: S-bound D = (p `2 ) - r
r > 0 by A1, TBSP_1:17;
then A3: (p `2 ) + 0 < (p `2 ) + r by XREAL_1:8;
(p `2 ) - r < (p `2 ) - 0 by A1, TBSP_1:17, XREAL_1:17;
then (p `2 ) - r < (p `2 ) + r by A3, XXREAL_0:2;
then A4: lower_bound ].((p `2 ) - r),((p `2 ) + r).[ = (p `2 ) - r by Th22;
proj2 .: D = ].((p `2 ) - r),((p `2 ) + r).[ by A1, A2, Th52;
hence S-bound D = (p `2 ) - r by A4, SPRECT_1:49; :: thesis: verum