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);
circle a,b,r = {}

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {} c= circle a,b,r

let x be set ; :: thesis: ( x in circle a,b,r implies x in {} )
assume x in circle a,b,r ; :: thesis: x in {}
then ex p being Point of (TOP-REAL 2) st
( x = p & |.(p - |[a,b]|).| = r ) ;
hence x in {} by A1; :: thesis: verum

end;

thus {} c= circle a,b,r by XBOOLE_1:2; :: thesis: verum

end;

hence circle a,b,r is compact ; :: thesis: verum

end;

suppose r > 0 ; :: thesis: circle a,b,r is compact

hence circle a,b,r is compact by Th31, Th32; :: thesis: verum

end;

suppose A2: 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
A3: x = p and
A4: |.(p - |[a,b]|).| = r ;
p = |[a,b]| by A2, A4, TOPRNS_1:29;
hence x in {|[a,b]|} by A3, 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 A5: x = |[a,b]| by TARSKI:def 1;
|.(|[a,b]| - |[a,b]|).| = 0 by TOPRNS_1:29;
hence x in circle a,b,r by A2, A5; :: thesis: verum

end;

hence circle a,b,r is compact ; :: thesis: verum

end;

end;