let a, b, r be real number ; :: thesis: for x being Point of (Euclid 2) st x = |[a,b]| holds
Ball x,r = inside_of_circle a,b,r
let x be Point of (Euclid 2); :: thesis: ( x = |[a,b]| implies Ball x,r = inside_of_circle a,b,r )
assume A1:
x = |[a,b]|
; :: thesis: Ball x,r = inside_of_circle a,b,r
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: inside_of_circle a,b,r c= Ball x,r
let w be
set ;
:: thesis: ( w in Ball x,r implies w in inside_of_circle a,b,r )assume A2:
w in Ball x,
r
;
:: thesis: w in inside_of_circle a,b,rthen reconsider u =
w as
Point of
(TOP-REAL 2) by TOPREAL3:13;
reconsider e =
u as
Point of
(Euclid 2) by TOPREAL3:13;
dist e,
x = |.(u - |[a,b]|).|
by A1, JGRAPH_1:45;
then
|.(u - |[a,b]|).| < r
by A2, METRIC_1:12;
hence
w in inside_of_circle a,
b,
r
by Th45;
:: thesis: verum
end;
let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in inside_of_circle a,b,r or w in Ball x,r )
assume A3:
w in inside_of_circle a,b,r
; :: thesis: w in Ball x,r
then reconsider u = w as Point of (TOP-REAL 2) ;
reconsider e = u as Point of (Euclid 2) by TOPREAL3:13;
dist e,x = |.(u - |[a,b]|).|
by A1, JGRAPH_1:45;
then
dist e,x < r
by A3, Th45;
hence
w in Ball x,r
by METRIC_1:12; :: thesis: verum