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