set Cb = circle a,b,r;
A1: ( |[r,0 ]| `1 = r & |[r,0 ]| `2 = 0 ) by EUCLID:56;
|.(|[(r + a),b]| - |[a,b]|).| = |.(|[(r + a),(0 + b)]| - |[a,b]|).|
.= |.((|[r,0 ]| + |[a,b]|) - |[a,b]|).| by EUCLID:60
.= |.(|[r,0 ]| + (|[a,b]| - |[a,b]|)).| by EUCLID:49
.= |.(|[r,0 ]| + (0. (TOP-REAL 2))).| by EUCLID:46
.= |.|[r,0 ]|.| by EUCLID:31
.= sqrt ((r ^2 ) + (0 ^2 )) by A1, JGRAPH_3:10
.= r by SQUARE_1:89 ;
then |[(r + a),b]| in circle a,b,r ;
hence not circle a,b,r is empty ; :: thesis: verum