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 number 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 number 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 number st P = Ball e,r & p = e holds
proj2 .: P = ].((p `2 ) - r),((p `2 ) + r).[
let r be real number ; :: 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 set ; :: 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 set such that
A3: x in the carrier of (TOP-REAL 2) and
A4: x in P and
A5: a = proj2 . x by FUNCT_2:115;
reconsider x = x as Point of (TOP-REAL 2) by A3;
reconsider b = a as Real by A5;
a = x `2 by A5, PSCOMP_1:def 29;
then ( (p `2 ) - r < b & b < (p `2 ) + r ) by A1, A2, A4, Th48;
hence a in ].((p `2 ) - r),((p `2 ) + r).[ by XXREAL_1:4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in ].((p `2 ) - r),((p `2 ) + r).[ or a in proj2 .: P )
assume A6: a in ].((p `2 ) - r),((p `2 ) + r).[ ; :: thesis: a in proj2 .: P
then reconsider b = a as Real ;
b < (p `2 ) + r by A6, XXREAL_1:4;
then A7: b - (p `2 ) < ((p `2 ) + r) - (p `2 ) by XREAL_1:11;
A8: a = |[(p `1 ),b]| `2 by EUCLID:56
.= proj2 . |[(p `1 ),b]| by PSCOMP_1:def 29 ;
reconsider f = |[(p `1 ),b]| as Point of (Euclid 2) by TOPREAL3:13;
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:12
.= sqrt ((((p `1 ) - (p `1 )) ^2 ) + (((|[(p `1 ),b]| `2 ) - (p `2 )) ^2 )) by EUCLID:56
.= sqrt (0 + ((b - (p `2 )) ^2 )) by EUCLID:56 ;

now

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 A7, A9, SQUARE_1:89; :: thesis: verum

end;

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

then A10: - (b - (p `2 )) > 0 by XREAL_1:60;
A11: sqrt ((b - (p `2 )) ^2 ) = sqrt ((- (b - (p `2 ))) ^2 )
.= - (b - (p `2 )) by A10, SQUARE_1:89 ;
(p `2 ) - r < b by A6, XXREAL_1:4;
then ((p `2 ) - r) + r < b + r by XREAL_1:8;
then (p `2 ) - b < (r + b) - b by XREAL_1:11;
hence dist f,e < r by A9, A11; :: thesis: verum

end;

end;

end;

then |[(p `1 ),b]| in P by A1, METRIC_1:12;
hence a in proj2 .: P by A8, FUNCT_2:43; :: thesis: verum