let a, b, r be real number ; :: thesis: for x being Point of (Euclid 2) st x = |[a,b]| holds
cl_Ball x,r = closed_inside_of_circle a,b,r
let x be Point of (Euclid 2); :: thesis: ( x = |[a,b]| implies cl_Ball x,r = closed_inside_of_circle a,b,r )
assume A1:
x = |[a,b]|
; :: thesis: cl_Ball x,r = closed_inside_of_circle a,b,r
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: closed_inside_of_circle a,b,r c= cl_Ball x,r
let w be
set ;
:: thesis: ( w in cl_Ball x,r implies w in closed_inside_of_circle a,b,r )assume A2:
w in cl_Ball x,
r
;
:: thesis: w in closed_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:13;
hence
w in closed_inside_of_circle a,
b,
r
by Th44;
:: thesis: verum
end;
let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in closed_inside_of_circle a,b,r or w in cl_Ball x,r )
assume A3:
w in closed_inside_of_circle a,b,r
; :: thesis: w in cl_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, Th44;
hence
w in cl_Ball x,r
by METRIC_1:13; :: thesis: verum