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

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