set Cb = circle (a,b,r);

per cases
( r < 0 or r > 0 or r = 0 )
;

end;

suppose A1:
r < 0
; :: thesis: circle (a,b,r) is compact

circle (a,b,r) = {}

end;proof

end;

hence
circle (a,b,r) is compact
; :: thesis: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {} c= circle (a,b,r)

thus
{} c= circle (a,b,r)
; :: thesis: verumlet 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;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

suppose A2:
r = 0
; :: thesis: circle (a,b,r) is compact

circle (a,b,r) = {|[a,b]|}

end;proof

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: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {|[a,b]|} c= circle (a,b,r)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {|[a,b]|} or x in 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;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

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