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

circle (a,b,r) = {}

proof

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

let x be object ; :: 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) ; :: 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 Th22, Th23; :: 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 object ; :: 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:28;
hence x in {|[a,b]|} by A3, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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:28;
hence x in circle (a,b,r) by A2, A5; :: thesis: verum

end;

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

end;

end;