The abstract of the Mizar article:

The Topological Space $\calE^2_\rmT$. Simple Closed Curves

by

Agata Darmochwal, and

Yatsuka Nakamura

Received December 30, 1991

MML identifier: TOPREAL2

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, EUCLID, FINSEQ_1, TOPREAL1, MCART_1, BOOLE, COMPTS_1,
      BORSUK_1, RELAT_1, TOPS_2, ORDINAL2, SUBSET_1, FUNCT_1, RCOMP_1,
      PCOMPS_1, FUNCT_4, TOPREAL2, FINSEQ_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2,
      FUNCT_4, STRUCT_0, GRCAT_1, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1,
      FINSEQ_1, FINSEQ_4, PCOMPS_1, EUCLID, TOPMETR, TOPREAL1;
 constructors TOPS_2, COMPTS_1, RCOMP_1, TOPMETR, TOPREAL1, FINSEQ_4, GRCAT_1,
      XCMPLX_0, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, PRE_TOPC, RELSET_1, STRUCT_0, EUCLID, BORSUK_1,
      TOPREAL1, XREAL_0, XBOOLE_0, MEMBERED, ZFMISC_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET;


begin

reserve a for set;
reserve p,p1,p2,q,q1,q2 for Point of TOP-REAL 2;
reserve h1,h2 for FinSequence of TOP-REAL 2;

theorem :: TOPREAL2:1
 p1 <> p2 & p1 in R^2-unit_square & p2 in R^2-unit_square implies
  ex P1, P2 being non empty Subset of TOP-REAL 2
   st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 &
   R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2};

theorem :: TOPREAL2:2
R^2-unit_square is compact;

theorem :: TOPREAL2:3
for Q, P being non empty Subset of TOP-REAL 2
 for f being map of (TOP-REAL 2)|Q, (TOP-REAL 2)|P st f is_homeomorphism &
  Q is_an_arc_of q1,q2 holds
  for p1, p2 st p1 = f.q1 & p2 = f.q2 holds P is_an_arc_of p1,p2;

definition let P be Subset of TOP-REAL 2;
  attr P is being_simple_closed_curve means
:: TOPREAL2:def 1

 ex f being map of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|P
    st f is_homeomorphism;
  synonym P is_simple_closed_curve;
end;

definition
 cluster R^2-unit_square -> being_simple_closed_curve;
end;

definition
 cluster being_simple_closed_curve Subset of TOP-REAL 2;
end;

definition
 mode Simple_closed_curve is being_simple_closed_curve Subset of TOP-REAL 2;
end;

theorem :: TOPREAL2:4
for P being non empty Subset of TOP-REAL 2 st
 P is_simple_closed_curve ex p1,p2 st p1 <> p2 & p1 in P & p2 in P;

theorem :: TOPREAL2:5
for P being non empty Subset of TOP-REAL 2 holds
P is_simple_closed_curve iff
 (ex p1,p2 st p1 <> p2 & p1 in P & p2 in P)
 & for p1,p2 st p1 <> p2 & p1 in P & p2 in P
    ex P1,P2 being non empty Subset of TOP-REAL 2
     st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 &
     P = P1 \/ P2 & P1 /\ P2 = {p1,p2};

theorem :: TOPREAL2:6
  for P being non empty Subset of TOP-REAL 2 holds
P is_simple_closed_curve iff
ex p1,p2 being Point of TOP-REAL 2,
   P1,P2 being non empty Subset of TOP-REAL 2
  st p1 <> p2 & p1 in P & p2 in P &
    P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 &
    P = P1 \/ P2 & P1 /\ P2 = {p1,p2};