consider x being Point of (TOP-REAL 2), r being real positive number ;
take Tcircle (x,r) ; :: thesis: ( Tcircle (x,r) is being_simple_closed_curve & Tcircle (x,r) is strict )
thus ( Tcircle (x,r) is being_simple_closed_curve & Tcircle (x,r) is strict ) ; :: thesis: verum