let p be Point of (TOP-REAL 2); :: thesis: for G being Subset of (TOP-REAL 2) st G is open & p in G holds
ex r being Real st
( r > 0 & { q where q is Point of (TOP-REAL 2) : ( (p `1) - r < q `1 & q `1 < (p `1) + r & (p `2) - r < q `2 & q `2 < (p `2) + r ) } c= G )
let G be Subset of (TOP-REAL 2); :: thesis: ( G is open & p in G implies ex r being Real st
( r > 0 & { q where q is Point of (TOP-REAL 2) : ( (p `1) - r < q `1 & q `1 < (p `1) + r & (p `2) - r < q `2 & q `2 < (p `2) + r ) } c= G ) )
assume that
A1: G is open and
A2: p in G ; :: thesis: ex r being Real st
( r > 0 & { q where q is Point of (TOP-REAL 2) : ( (p `1) - r < q `1 & q `1 < (p `1) + r & (p `2) - r < q `2 & q `2 < (p `2) + r ) } c= G )
reconsider GG = G as Subset of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) ;
reconsider q2 = p as Point of (Euclid 2) by TOPREAL3:8;
( TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) & GG is open ) by A1, EUCLID:def 8, PRE_TOPC:30;
then consider r being Real such that
A3: r > 0 and
A4: Ball (q2,r) c= GG by A2, TOPMETR:15;
set s = r / (sqrt 2);
A5: Ball (q2,r) = { q3 where q3 is Point of (TOP-REAL 2) : |.(p - q3).| < r } by Th2;
A6: { q where q is Point of (TOP-REAL 2) : ( (p `1) - (r / (sqrt 2)) < q `1 & q `1 < (p `1) + (r / (sqrt 2)) & (p `2) - (r / (sqrt 2)) < q `2 & q `2 < (p `2) + (r / (sqrt 2)) ) } c= Ball (q2,r)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( (p `1) - (r / (sqrt 2)) < q `1 & q `1 < (p `1) + (r / (sqrt 2)) & (p `2) - (r / (sqrt 2)) < q `2 & q `2 < (p `2) + (r / (sqrt 2)) ) } or x in Ball (q2,r) )
assume x in { q where q is Point of (TOP-REAL 2) : ( (p `1) - (r / (sqrt 2)) < q `1 & q `1 < (p `1) + (r / (sqrt 2)) & (p `2) - (r / (sqrt 2)) < q `2 & q `2 < (p `2) + (r / (sqrt 2)) ) } ; :: thesis: x in Ball (q2,r)
then consider q being Point of (TOP-REAL 2) such that
A7: q = x and
A8: (p `1) - (r / (sqrt 2)) < q `1 and
A9: q `1 < (p `1) + (r / (sqrt 2)) and
A10: (p `2) - (r / (sqrt 2)) < q `2 and
A11: q `2 < (p `2) + (r / (sqrt 2)) ;
((p `1) + (r / (sqrt 2))) - (r / (sqrt 2)) > (q `1) - (r / (sqrt 2)) by A9, XREAL_1:14;
then A12: (p `1) - (q `1) > ((q `1) + (- (r / (sqrt 2)))) - (q `1) by XREAL_1:14;
((p `2) + (r / (sqrt 2))) - (r / (sqrt 2)) > (q `2) - (r / (sqrt 2)) by A11, XREAL_1:14;
then A13: (p `2) - (q `2) > ((q `2) + (- (r / (sqrt 2)))) - (q `2) by XREAL_1:14;
((p `2) - (r / (sqrt 2))) + (r / (sqrt 2)) < (q `2) + (r / (sqrt 2)) by A10, XREAL_1:8;
then (p `2) - (q `2) < ((q `2) + (r / (sqrt 2))) - (q `2) by XREAL_1:14;
then A14: ((p `2) - (q `2)) ^2 < (r / (sqrt 2)) ^2 by A13, SQUARE_1:50;
(r / (sqrt 2)) ^2 = (r ^2) / ((sqrt 2) ^2) by XCMPLX_1:76
.= (r ^2) / 2 by SQUARE_1:def 2 ;
then A15: ((r / (sqrt 2)) ^2) + ((r / (sqrt 2)) ^2) = r ^2 ;
((p `1) - (r / (sqrt 2))) + (r / (sqrt 2)) < (q `1) + (r / (sqrt 2)) by A8, XREAL_1:8;
then (p `1) - (q `1) < ((q `1) + (r / (sqrt 2))) - (q `1) by XREAL_1:14;
then A16: ( (p - q) `2 = (p `2) - (q `2) & ((p `1) - (q `1)) ^2 < (r / (sqrt 2)) ^2 ) by A12, SQUARE_1:50, TOPREAL3:3;
( |.(p - q).| ^2 = (((p - q) `1) ^2) + (((p - q) `2) ^2) & (p - q) `1 = (p `1) - (q `1) ) by JGRAPH_1:29, TOPREAL3:3;
then |.(p - q).| ^2 < r ^2 by A16, A14, A15, XREAL_1:8;
then |.(p - q).| < r by A3, SQUARE_1:48;
hence x in Ball (q2,r) by A5, A7; :: thesis: verum

end;

r / (sqrt 2) > 0 by A3, XREAL_1:139;
hence ex r being Real st
( r > 0 & { q where q is Point of (TOP-REAL 2) : ( (p `1) - r < q `1 & q `1 < (p `1) + r & (p `2) - r < q `2 & q `2 < (p `2) + r ) } c= G ) by A4, A6, XBOOLE_1:1; :: thesis: verum