set Cb = circle (a,b,r);
A1:
|[r,0]| `1 = r
by EUCLID:52;
A2:
|[r,0]| `2 = 0
by EUCLID:52;
|.(|[(r + a),b]| - |[a,b]|).| =
|.(|[(r + a),(0 + b)]| - |[a,b]|).|
.=
|.((|[r,0]| + |[a,b]|) - |[a,b]|).|
by EUCLID:56
.=
|.(|[r,0]| + (|[a,b]| - |[a,b]|)).|
by RLVECT_1:def 3
.=
|.(|[r,0]| + (0. (TOP-REAL 2))).|
by RLVECT_1:5
.=
|.|[r,0]|.|
by RLVECT_1:4
.=
sqrt ((r ^2) + (0 ^2))
by A1, A2, JGRAPH_3:1
.=
r
by SQUARE_1:22
;
then
|[(r + a),b]| in circle (a,b,r)
;
hence
not circle (a,b,r) is empty
; verum