set Cb = circle a,b,r;
per cases
( r < 0 or r > 0 or r = 0 )
;
suppose A1:
r < 0
;
:: thesis: circle a,b,r is compact set A =
(TOP-REAL 2) | (circle a,b,r);
A2:
circle a,
b,
r = {}
then A3:
circle a,
b,
r c= [#] ((TOP-REAL 2) | (circle a,b,r))
;
for
P being
Subset of
((TOP-REAL 2) | (circle a,b,r)) st
P = circle a,
b,
r holds
P is
compact
by A2;
hence
circle a,
b,
r is
compact
by A3, COMPTS_1:11;
:: thesis: verum end; suppose A5:
r = 0
;
:: thesis: circle a,b,r is compact
circle a,
b,
r = {|[a,b]|}
proof
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: {|[a,b]|} c= circle a,b,r
let x be
set ;
:: thesis: ( x in circle a,b,r implies x in {|[a,b]|} )assume
x in circle a,
b,
r
;
:: thesis: x in {|[a,b]|}then consider p being
Point of
(TOP-REAL 2) such that A6:
x = p
and A7:
|.(p - |[a,b]|).| = r
;
p = |[a,b]|
by A5, A7, TOPRNS_1:29;
hence
x in {|[a,b]|}
by A6, TARSKI:def 1;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {|[a,b]|} or x in circle a,b,r )
assume
x in {|[a,b]|}
;
:: thesis: x in circle a,b,r
then A8:
x = |[a,b]|
by TARSKI:def 1;
|.(|[a,b]| - |[a,b]|).| = 0
by TOPRNS_1:29;
hence
x in circle a,
b,
r
by A5, A8;
:: thesis: verum
end; hence
circle a,
b,
r is
compact
;
:: thesis: verum end;