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