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

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