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

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