reconsider e = x as Point of (Euclid n) by TOPREAL3:8;
n in NAT by ORDINAL1:def 12;
then the carrier of (Tcircle (x,r)) = Sphere (x,r) by Th9
.= Sphere (e,r) by TOPREAL9:15
.= {e} by TOPREAL6:54 ;
hence Tcircle (x,r) is trivial ; :: thesis: verum