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 number 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 number 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 A1: ( G is open & p in G ) ; :: thesis: ex r being real number 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 q2 = p as Point of (Euclid 2) by TOPREAL3:13;
X: TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) by EUCLID:def 8;
reconsider GG = G as Subset of TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) ;
GG is open by A1, PRE_TOPC:60;
then consider r being real number such that
A2: ( r > 0 & Ball q2,r c= GG ) by A1, TOPMETR:22, X;
set s = r / (sqrt 2);
sqrt 2 > 0 by SQUARE_1:93;
then A3: r / (sqrt 2) > 0 by A2, XREAL_1:141;
A4: Ball q2,r = { q3 where q3 is Point of (TOP-REAL 2) : |.(p - q3).| < r } by Th10;
{ 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 set ; :: 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
A5: ( q = x & (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)) ) ;
A6: |.(p - q).| ^2 = (((p - q) `1 ) ^2 ) + (((p - q) `2 ) ^2 ) by JGRAPH_1:46;
A7: ( (p - q) `1 = (p `1 ) - (q `1 ) & (p - q) `2 = (p `2 ) - (q `2 ) ) by TOPREAL3:8;
((p `1 ) - (r / (sqrt 2))) + (r / (sqrt 2)) < (q `1 ) + (r / (sqrt 2)) by A5, XREAL_1:10;
then A8: (p `1 ) - (q `1 ) < ((q `1 ) + (r / (sqrt 2))) - (q `1 ) by XREAL_1:16;
((p `1 ) + (r / (sqrt 2))) - (r / (sqrt 2)) > (q `1 ) - (r / (sqrt 2)) by A5, XREAL_1:16;
then (p `1 ) - (q `1 ) > ((q `1 ) + (- (r / (sqrt 2)))) - (q `1 ) by XREAL_1:16;
then A9: ((p `1 ) - (q `1 )) ^2 < (r / (sqrt 2)) ^2 by A8, SQUARE_1:120;
((p `2 ) - (r / (sqrt 2))) + (r / (sqrt 2)) < (q `2 ) + (r / (sqrt 2)) by A5, XREAL_1:10;
then A10: (p `2 ) - (q `2 ) < ((q `2 ) + (r / (sqrt 2))) - (q `2 ) by XREAL_1:16;
((p `2 ) + (r / (sqrt 2))) - (r / (sqrt 2)) > (q `2 ) - (r / (sqrt 2)) by A5, XREAL_1:16;
then (p `2 ) - (q `2 ) > ((q `2 ) + (- (r / (sqrt 2)))) - (q `2 ) by XREAL_1:16;
then A11: ((p `2 ) - (q `2 )) ^2 < (r / (sqrt 2)) ^2 by A10, SQUARE_1:120;
(r / (sqrt 2)) ^2 = (r ^2 ) / ((sqrt 2) ^2 ) by XCMPLX_1:77
.= (r ^2 ) / 2 by SQUARE_1:def 4 ;
then ((r / (sqrt 2)) ^2 ) + ((r / (sqrt 2)) ^2 ) = r ^2 ;
then |.(p - q).| ^2 < r ^2 by A6, A7, A9, A11, XREAL_1:10;
then |.(p - q).| < r by A2, SQUARE_1:118;
hence x in Ball q2,r by A4, A5; :: thesis: verum

end;

hence ex r being real number 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 A2, A3, XBOOLE_1:1; :: thesis: verum