environ vocabulary REALSET1, FINSEQ_1, BOOLE, RELAT_1, FINSEQ_5, MATRIX_1, GOBOARD1, FINSEQ_4, RFINSEQ, COMPTS_1, RELAT_2, SPPOL_1, EUCLID, JORDAN1E, JORDAN8, JORDAN9, FINSEQ_6, PSCOMP_1, TOPREAL1, GOBOARD5, MCART_1, TREES_1, FUNCT_1, ARYTM_1, CARD_1, PRE_TOPC, ARYTM_3, GROUP_1, JORDAN1A, SPPOL_2, JORDAN3, SPRECT_2, GROUP_2, JORDAN5C, JORDAN6; notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XREAL_0, REAL_1, NAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1, REALSET1, FINSEQ_6, STRUCT_0, PRE_TOPC, CARD_1, CARD_4, BINARITH, CONNSP_1, COMPTS_1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3, JORDAN8, JORDAN5C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E; constructors JORDAN8, REALSET1, JORDAN6, REAL_1, CARD_4, PSCOMP_1, BINARITH, CONNSP_1, JORDAN9, JORDAN1A, WSIERP_1, FINSEQ_4, GOBRD13, JORDAN3, RFINSEQ, TOPS_2, TOPMETR, TOPREAL2, JORDAN5C, SPRECT_1, FINSEQ_5, ENUMSET1, FINSOP_1, JORDAN1E, INT_1; clusters XREAL_0, SPRECT_1, TOPREAL6, JORDAN8, REVROT_1, RELSET_1, ARYTM_3, SUBSET_1, FINSEQ_6, SPRECT_3, AMISTD_1, GOBOARD1, FINSEQ_1, FINSEQ_5, SPPOL_2, JORDAN1A, GOBOARD4, JORDAN1E, BINARITH, REALSET1, MEMBERED, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin reserve n for Nat; definition cluster trivial FinSequence; end; theorem :: JORDAN1G:1 for f be trivial FinSequence holds f is empty or ex x be set st f = <*x*>; definition let p be non trivial FinSequence; cluster Rev p -> non trivial; end; theorem :: JORDAN1G:2 for D be non empty set for f be FinSequence of D for G be Matrix of D for p be set holds f is_sequence_on G implies f-:p is_sequence_on G; theorem :: JORDAN1G:3 for D be non empty set for f be FinSequence of D for G be Matrix of D for p be Element of D st p in rng f holds f is_sequence_on G implies f:-p is_sequence_on G; theorem :: JORDAN1G:4 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Upper_Seq(C,n) is_sequence_on Gauge(C,n); theorem :: JORDAN1G:5 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Lower_Seq(C,n) is_sequence_on Gauge(C,n); definition let C be compact connected non vertical non horizontal Subset of TOP-REAL 2; let n be Nat; cluster Upper_Seq(C,n) -> standard; cluster Lower_Seq(C,n) -> standard; end; theorem :: JORDAN1G:6 for G be Y_equal-in-column Y_increasing-in-line Matrix of TOP-REAL 2 for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds G*(i1,j1)`2 = G*(i2,j2)`2 implies j1 = j2; theorem :: JORDAN1G:7 for G be X_equal-in-line X_increasing-in-column Matrix of TOP-REAL 2 for i1,i2,j1,j2 be Nat st [i1,j1] in Indices G & [i2,j2] in Indices G holds G*(i1,j1)`1 = G*(i2,j2)`1 implies i1 = i2; canceled 8; theorem :: JORDAN1G:16 for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or (f/.1 <> N-max L~f & f/.len f <> N-max L~f) holds (N-min L~f)`1 < (N-max L~f)`1; theorem :: JORDAN1G:17 for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> N-min L~f & f/.len f <> N-min L~f) or (f/.1 <> N-max L~f & f/.len f <> N-max L~f) holds N-min L~f <> N-max L~f; theorem :: JORDAN1G:18 for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or (f/.1 <> S-max L~f & f/.len f <> S-max L~f) holds (S-min L~f)`1 < (S-max L~f)`1; theorem :: JORDAN1G:19 for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> S-min L~f & f/.len f <> S-min L~f) or (f/.1 <> S-max L~f & f/.len f <> S-max L~f) holds S-min L~f <> S-max L~f; theorem :: JORDAN1G:20 for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or (f/.1 <> W-max L~f & f/.len f <> W-max L~f) holds (W-min L~f)`2 < (W-max L~f)`2; theorem :: JORDAN1G:21 for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> W-min L~f & f/.len f <> W-min L~f) or (f/.1 <> W-max L~f & f/.len f <> W-max L~f) holds W-min L~f <> W-max L~f; theorem :: JORDAN1G:22 for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or (f/.1 <> E-max L~f & f/.len f <> E-max L~f) holds (E-min L~f)`2 < (E-max L~f)`2; theorem :: JORDAN1G:23 for f be standard special unfolded (non trivial FinSequence of TOP-REAL 2) st (f/.1 <> E-min L~f & f/.len f <> E-min L~f) or (f/.1 <> E-max L~f & f/.len f <> E-max L~f) holds E-min L~f <> E-max L~f; theorem :: JORDAN1G:24 for D be non empty set for f be FinSequence of D for p,q be Element of D st p in rng f & q in rng f & q..f <= p..f holds (f-:p):-q = (f:-q)-:p; theorem :: JORDAN1G:25 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds L~(Cage(C,n)-:W-min L~Cage(C,n)) /\ L~(Cage(C,n):-W-min L~Cage(C,n)) = {N-min L~Cage(C,n),W-min L~Cage(C,n)}; theorem :: JORDAN1G:26 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds Lower_Seq(C,n) = Rotate(Cage(C,n),E-max L~Cage(C,n))-:W-min L~Cage(C,n); theorem :: JORDAN1G:27 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (W-min L~Cage(C,n))..Upper_Seq(C,n) = 1; theorem :: JORDAN1G:28 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (W-min L~Cage(C,n))..Upper_Seq(C,n) < (W-max L~Cage(C,n))..Upper_Seq(C,n); theorem :: JORDAN1G:29 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (W-max L~Cage(C,n))..Upper_Seq(C,n) <= (N-min L~Cage(C,n))..Upper_Seq(C,n); theorem :: JORDAN1G:30 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (N-min L~Cage(C,n))..Upper_Seq(C,n) < (N-max L~Cage(C,n))..Upper_Seq(C,n); theorem :: JORDAN1G:31 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (N-max L~Cage(C,n))..Upper_Seq(C,n) <= (E-max L~Cage(C,n))..Upper_Seq(C,n); theorem :: JORDAN1G:32 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (E-max L~Cage(C,n))..Upper_Seq(C,n) = len Upper_Seq(C,n); theorem :: JORDAN1G:33 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds (E-max L~Cage(C,n))..Lower_Seq(C,n) = 1; theorem :: JORDAN1G:34 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (E-max L~Cage(C,n))..Lower_Seq(C,n) < (E-min L~Cage(C,n))..Lower_Seq(C,n); theorem :: JORDAN1G:35 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (E-min L~Cage(C,n))..Lower_Seq(C,n) <= (S-max L~Cage(C,n))..Lower_Seq(C,n); theorem :: JORDAN1G:36 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (S-max L~Cage(C,n))..Lower_Seq(C,n) < (S-min L~Cage(C,n))..Lower_Seq(C,n); theorem :: JORDAN1G:37 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (S-min L~Cage(C,n))..Lower_Seq(C,n) <= (W-min L~Cage(C,n))..Lower_Seq(C,n); theorem :: JORDAN1G:38 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (W-min L~Cage(C,n))..Lower_Seq(C,n) = len Lower_Seq(C,n); theorem :: JORDAN1G:39 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (Upper_Seq(C,n)/.2)`1 = W-bound L~Cage(C,n); theorem :: JORDAN1G:40 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds (Lower_Seq(C,n)/.2)`1 = E-bound L~Cage(C,n); theorem :: JORDAN1G:41 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds W-bound L~Cage(C,n) + E-bound L~Cage(C,n) = W-bound C + E-bound C; theorem :: JORDAN1G:42 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 holds S-bound L~Cage(C,n) + N-bound L~Cage(C,n) = S-bound C + N-bound C; theorem :: JORDAN1G:43 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n,i be Nat st 1 <= i & i <= width Gauge(C,n) & n > 0 holds Gauge(C,n)*(Center Gauge(C,n),i)`1 = (W-bound C + E-bound C) / 2; theorem :: JORDAN1G:44 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n,i be Nat st 1 <= i & i <= len Gauge(C,n) & n > 0 holds Gauge(C,n)*(i,Center Gauge(C,n))`2 = (S-bound C + N-bound C) / 2; theorem :: JORDAN1G:45 for f be S-Sequence_in_R2 for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f/.1 in L~mid(f,k1,k2) holds k1 = 1 or k2 = 1; theorem :: JORDAN1G:46 for f be S-Sequence_in_R2 for k1,k2 be Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f/.(len f) in L~mid(f,k1,k2) holds k1 = len f or k2 = len f; theorem :: JORDAN1G:47 for C be compact non vertical non horizontal Subset of TOP-REAL 2 for n be Nat holds rng Upper_Seq(C,n) c= rng Cage(C,n) & rng Lower_Seq(C,n) c= rng Cage(C,n); theorem :: JORDAN1G:48 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds Upper_Seq(C,n) is_a_h.c._for Cage(C,n); theorem :: JORDAN1G:49 for C be compact non vertical non horizontal Subset of TOP-REAL 2 holds Rev Lower_Seq(C,n) is_a_h.c._for Cage(C,n); theorem :: JORDAN1G:50 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 < i & i <= len Gauge(C,n) holds not Gauge(C,n)*(i,1) in rng Upper_Seq(C,n); theorem :: JORDAN1G:51 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 <= i & i < len Gauge(C,n) holds not Gauge(C,n)*(i,width Gauge(C,n)) in rng Lower_Seq(C,n); theorem :: JORDAN1G:52 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 < i & i <= len Gauge(C,n) holds not Gauge(C,n)*(i,1) in L~Upper_Seq(C,n); theorem :: JORDAN1G:53 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i be Nat st 1 <= i & i < len Gauge(C,n) holds not Gauge(C,n)*(i,width Gauge(C,n)) in L~Lower_Seq(C,n); theorem :: JORDAN1G:54 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,j)) meets L~Lower_Seq(C,n); theorem :: JORDAN1G:55 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)) in rng Upper_Seq(C,n); theorem :: JORDAN1G:56 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)) in rng Lower_Seq(C,n); theorem :: JORDAN1G:57 for f be S-Sequence_in_R2 for p be Point of TOP-REAL 2 st p in rng f holds R_Cut(f,p) = mid(f,1,p..f); theorem :: JORDAN1G:58 for f be S-Sequence_in_R2 for Q be closed Subset of TOP-REAL 2 st L~f meets Q & not f/.1 in Q & First_Point(L~f,f/.1,f/.len f,Q) in rng f holds L~mid(f,1,First_Point(L~f,f/.1,f/.len f,Q)..f) /\ Q = {First_Point(L~f,f/.1,f/.len f,Q)}; theorem :: JORDAN1G:59 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for k be Nat st 1 <= k & k < First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)).. Upper_Seq(C,n) holds (Upper_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; theorem :: JORDAN1G:60 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for k be Nat st 1 <= k & k < First_Point(L~Rev Lower_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2)).. Rev Lower_Seq(C,n) holds (Rev Lower_Seq(C,n)/.k)`1 < (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; theorem :: JORDAN1G:61 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for q be Point of TOP-REAL 2 holds q in rng mid(Upper_Seq(C,n),2,First_Point(L~Upper_Seq(C,n), W-min L~Cage(C,n),E-max L~Cage(C,n),Vertical_Line ((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))..Upper_Seq(C,n)) implies q`1 <= (W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2; theorem :: JORDAN1G:62 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds First_Point(L~Upper_Seq(C,n),W-min L~Cage(C,n),E-max L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2 > Last_Point(L~Lower_Seq(C,n),E-max L~Cage(C,n),W-min L~Cage(C,n), Vertical_Line((W-bound L~Cage(C,n)+E-bound L~Cage(C,n))/2))`2; theorem :: JORDAN1G:63 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds L~Upper_Seq(C,n) = Upper_Arc L~Cage(C,n); theorem :: JORDAN1G:64 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 holds L~Lower_Seq(C,n) = Lower_Arc L~Cage(C,n); theorem :: JORDAN1G:65 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for n be Nat st n > 0 for i,j be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Cage(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,j)) meets Lower_Arc L~Cage(C,n);