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;