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 ; :: thesis: verum