reconsider e = x as Point of (Euclid n) by TOPREAL3:13;
the carrier of (Tcircle x,r) = Sphere x,r by Th9
.= Sphere e,r by TOPREAL9:15
.= {e} by TOPREAL6:62 ;
hence Tcircle x,r is trivial ; :: thesis: verum