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 that
A1: G is open and
A2: 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 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:13;
( 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:60;
then consider r being real number such that
A3: r > 0 and
A4: Ball q2,r c= GG by A2, TOPMETR:22;
set s = r / (sqrt 2);
A5: Ball q2,r = { q3 where q3 is Point of (TOP-REAL 2) : |.(p - q3).| < r } by Th10;
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 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
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:16;
then A12: (p `1 ) - (q `1 ) > ((q `1 ) + (- (r / (sqrt 2)))) - (q `1 ) by XREAL_1:16;
((p `2 ) + (r / (sqrt 2))) - (r / (sqrt 2)) > (q `2 ) - (r / (sqrt 2)) by A11, XREAL_1:16;
then A13: (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 A10, XREAL_1:10;
then (p `2 ) - (q `2 ) < ((q `2 ) + (r / (sqrt 2))) - (q `2 ) by XREAL_1:16;
then A14: ((p `2 ) - (q `2 )) ^2 < (r / (sqrt 2)) ^2 by A13, 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 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:10;
then (p `1 ) - (q `1 ) < ((q `1 ) + (r / (sqrt 2))) - (q `1 ) by XREAL_1:16;
then A16: ( (p - q) `2 = (p `2 ) - (q `2 ) & ((p `1 ) - (q `1 )) ^2 < (r / (sqrt 2)) ^2 ) by A12, SQUARE_1:120, TOPREAL3:8;
( |.(p - q).| ^2 = (((p - q) `1 ) ^2 ) + (((p - q) `2 ) ^2 ) & (p - q) `1 = (p `1 ) - (q `1 ) ) by JGRAPH_1:46, TOPREAL3:8;
then |.(p - q).| ^2 < r ^2 by A16, A14, A15, XREAL_1:10;
then |.(p - q).| < r by A3, SQUARE_1:118;
hence x in Ball q2,r by A5, A7; :: thesis: verum

end;

sqrt 2 > 0 by SQUARE_1:93;
then r / (sqrt 2) > 0 by A3, XREAL_1:141;
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 A4, A6, XBOOLE_1:1; :: thesis: verum