per cases ( r is positive or not r is positive ) ;

suppose r is positive ; :: thesis: Tcircle (x,r) is pathwise_connected

then reconsider r = r as positive Real ;
Tcircle (x,r) is pathwise_connected ;
hence Tcircle (x,r) is pathwise_connected ; :: thesis: verum

end;

suppose not r is positive ; :: thesis: Tcircle (x,r) is pathwise_connected

then reconsider r = r as non positive non negative Real ;
Tcircle (x,r) is trivial ;
hence Tcircle (x,r) is pathwise_connected ; :: thesis: verum

end;

end;