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