let p be Point of (TOP-REAL 2); :: thesis: for e being Point of (Euclid 2)
for P being Subset of (TOP-REAL 2)
for r being Real st P = Ball (e,r) & p = e holds
proj2 .: P = ].((p `2) - r),((p `2) + r).[
let e be Point of (Euclid 2); :: thesis: for P being Subset of (TOP-REAL 2)
for r being Real st P = Ball (e,r) & p = e holds
proj2 .: P = ].((p `2) - r),((p `2) + r).[
let P be Subset of (TOP-REAL 2); :: thesis: for r being Real st P = Ball (e,r) & p = e holds
proj2 .: P = ].((p `2) - r),((p `2) + r).[
let r be Real; :: thesis: ( P = Ball (e,r) & p = e implies proj2 .: P = ].((p `2) - r),((p `2) + r).[ )
assume that
A1: P = Ball (e,r) and
A2: p = e ; :: thesis: proj2 .: P = ].((p `2) - r),((p `2) + r).[

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: ].((p `2) - r),((p `2) + r).[ c= proj2 .: P

let a be object ; :: thesis: ( a in proj2 .: P implies a in ].((p `2) - r),((p `2) + r).[ )
assume a in proj2 .: P ; :: thesis: a in ].((p `2) - r),((p `2) + r).[
then consider x being object such that
A3: x in the carrier of (TOP-REAL 2) and
A4: x in P and
A5: a = proj2 . x by FUNCT_2:64;
reconsider b = a as Real by A5;
reconsider x = x as Point of (TOP-REAL 2) by A3;
A6: a = x `2 by A5, PSCOMP_1:def 6;
then A7: b < (p `2) + r by A1, A2, A4, Th38;
(p `2) - r < b by A1, A2, A4, A6, Th38;
hence a in ].((p `2) - r),((p `2) + r).[ by A7, XXREAL_1:4; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ].((p `2) - r),((p `2) + r).[ or a in proj2 .: P )
assume A8: a in ].((p `2) - r),((p `2) + r).[ ; :: thesis: a in proj2 .: P
then reconsider b = a as Real ;
reconsider f = |[(p `1),b]| as Point of (Euclid 2) by TOPREAL3:8;
A9: dist (f,e) = (Pitag_dist 2) . (f,e) by METRIC_1:def 1
.= sqrt ((((|[(p `1),b]| `1) - (p `1)) ^2) + (((|[(p `1),b]| `2) - (p `2)) ^2)) by A2, TOPREAL3:7
.= sqrt ((((p `1) - (p `1)) ^2) + (((|[(p `1),b]| `2) - (p `2)) ^2))
.= sqrt (0 + ((b - (p `2)) ^2)) ;
b < (p `2) + r by A8, XXREAL_1:4;
then A10: b - (p `2) < ((p `2) + r) - (p `2) by XREAL_1:9;

now :: thesis: ( ( 0 <= b - (p `2) & dist (f,e) < r ) or ( 0 > b - (p `2) & dist (f,e) < r ) )

per cases ( 0 <= b - (p `2) or 0 > b - (p `2) ) ;

case 0 <= b - (p `2) ; :: thesis: dist (f,e) < r

hence dist (f,e) < r by A10, A9, SQUARE_1:22; :: thesis: verum

end;

case A11: 0 > b - (p `2) ; :: thesis: dist (f,e) < r

(p `2) - r < b by A8, XXREAL_1:4;
then ((p `2) - r) + r < b + r by XREAL_1:6;
then A12: (p `2) - b < (r + b) - b by XREAL_1:9;
sqrt ((b - (p `2)) ^2) = sqrt ((- (b - (p `2))) ^2)
.= - (b - (p `2)) by A11, SQUARE_1:22 ;
hence dist (f,e) < r by A9, A12; :: thesis: verum

end;

end;

end;

then A13: |[(p `1),b]| in P by A1, METRIC_1:11;
a = |[(p `1),b]| `2
.= proj2 . |[(p `1),b]| by PSCOMP_1:def 6 ;
hence a in proj2 .: P by A13, FUNCT_2:35; :: thesis: verum