set x = the Point of (TOP-REAL 2);
set r = the positive Real;
take Tcircle ( the Point of (TOP-REAL 2), the positive Real) ; :: thesis: ( Tcircle ( the Point of (TOP-REAL 2), the positive Real) is being_simple_closed_curve & Tcircle ( the Point of (TOP-REAL 2), the positive Real) is strict )
thus ( Tcircle ( the Point of (TOP-REAL 2), the positive Real) is being_simple_closed_curve & Tcircle ( the Point of (TOP-REAL 2), the positive Real) is strict ) ; :: thesis: verum