The abstract of the Mizar article:

On the Components of the Complement of a Special Polygonal Curve

by

Andrzej Trybulec, and

Yatsuka Nakamura

Received January 21, 1999

MML identifier: SPRECT_4

[ Mizar article, MML identifier index ]

environ

 vocabulary COMPTS_1, PRE_TOPC, SPPOL_2, EUCLID, TOPREAL1, BOOLE, FINSEQ_4,
      JORDAN3, JORDAN5C, FINSEQ_1, GROUP_2, RELAT_1, FUNCT_1, ARYTM_1,
      SPRECT_2, SEQM_3, GOBOARD5, PSCOMP_1, GOBOARD9, SPRECT_1, GOBOARD2,
      TREES_1, MATRIX_1, ARYTM_3, TOPS_1, MCART_1, TOPREAL4, SPPOL_1, FINSEQ_5,
      FINSEQ_6;
 notation TARSKI, XBOOLE_0, XREAL_0, REAL_1, NAT_1, FUNCT_1, FINSEQ_1,
      FINSEQ_4, BINARITH, MATRIX_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1,
      EUCLID, TOPREAL1, TOPREAL4, FINSEQ_5, FINSEQ_6, GOBOARD1, GOBOARD2,
      SPPOL_1, SPPOL_2, GOBOARD5, GOBOARD9, JORDAN3, PSCOMP_1, JORDAN5C,
      SPRECT_1, SPRECT_2;
 constructors SPRECT_2, GOBOARD9, FINSEQ_4, JORDAN5C, TOPS_2, TOPMETR,
      BINARITH, COMPTS_1, TOPS_1, SPRECT_1, TOPREAL4, GOBOARD2, SPPOL_1,
      PSCOMP_1, JORDAN3, REAL_1, TOPREAL2, MATRIX_2, REALSET1, WAYBEL_3;
 clusters RELSET_1, SPRECT_1, SPPOL_2, GOBOARD2, FINSEQ_6, BORSUK_2, SPRECT_3,
      GOBOARD9, REVROT_1, ARYTM_3, PRE_TOPC, WAYBEL_3, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve i,j,l for Nat;

definition let T be being_T2 (non empty TopSpace);
 cluster compact -> closed Subset of T;
end;

theorem :: SPRECT_4:1
 for f being S-Sequence_in_R2, Q being closed Subset of TOP-REAL 2
  st L~f meets Q & not f/.1 in Q
holds L~R_Cut(f,First_Point(L~f,f/.1,f/.len f,Q)) /\ Q =
            { First_Point(L~f,f/.1,f/.len f,Q) };

theorem :: SPRECT_4:2
   for f being non empty FinSequence of TOP-REAL 2,
     p being Point of TOP-REAL 2 st f is_S-Seq & p = f/.len f holds
   L~L_Cut (f,p) = {};

canceled;

theorem :: SPRECT_4:4
 for f being S-Sequence_in_R2, p being Point of TOP-REAL 2, j st
   1 <=j & j < len f & p in L~mid(f,j,len f)
  holds LE f/.j, p, L~f, f/.1, f/.len f;

theorem :: SPRECT_4:5
 for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2, j st
   1 <=j & j < len f & p in LSeg(f,j) & q in LSeg(p,f/.(j+1))
  holds LE p, q, L~f, f/.1, f/.len f;

theorem :: SPRECT_4:6
 for f being S-Sequence_in_R2, Q being closed Subset of TOP-REAL 2
  st L~f meets Q & not f/.len f in Q
holds L~L_Cut(f,Last_Point(L~f,f/.1,f/.len f,Q)) /\ Q =
            { Last_Point(L~f,f/.1,f/.len f,Q) };

reserve q for Point of TOP-REAL 2;

theorem :: SPRECT_4:7
   for f being non constant standard special_circular_sequence
 holds LeftComp f <> RightComp f;