:: Properties of the Upper and Lower Sequence on the Cage :: by Robert Milewski :: :: Received August 1, 2002 :: Copyright (c) 2002-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, EUCLID, XBOOLE_0, RELAT_1, PRE_TOPC, MCART_1, FUNCT_1, TARSKI, JORDAN6, REAL_1, RCOMP_1, JORDAN2C, GOBOARD1, XXREAL_0, FINSEQ_1, TREES_1, RLTOPSP1, SPPOL_1, JORDAN1A, RELAT_2, JORDAN8, TOPREAL1, JORDAN1E, MATRIX_1, SEQ_4, PSCOMP_1, XXREAL_2, TOPREAL2, ARYTM_3, CARD_1, JORDAN9, JORDAN3, PARTFUN1, GOBOARD5, ARYTM_1, FINSEQ_4, GRAPH_2, FINSEQ_6, ZFMISC_1, GOBOARD9, GOBOARD2, FINSEQ_5, SPRECT_2, GROUP_2, NAT_1, CONNSP_1; notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, XXREAL_2, SEQ_4, MATRIX_0, FINSEQ_6, GRAPH_2, STRUCT_0, PRE_TOPC, RCOMP_1, TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, MEASURE6, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, JORDAN3, JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E; constructors REAL_1, RCOMP_1, FINSEQ_4, NEWTON, BINARITH, CONNSP_1, REALSET2, GOBOARD2, PSCOMP_1, GRAPH_2, GOBOARD9, JORDAN3, JORDAN5C, JORDAN6, JORDAN2C, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1, CONVEX1, MEASURE6; registrations XBOOLE_0, RELSET_1, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_6, STRUCT_0, COMPTS_1, TOPREAL1, TOPREAL2, GOBOARD2, JORDAN1, SPPOL_2, PSCOMP_1, GOBRD11, TOPREAL5, SPRECT_1, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1E, JORDAN1J, FUNCT_1, EUCLID, RLTOPSP1, MEASURE6, JORDAN5A, JORDAN2C, XREAL_0, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin reserve n for Nat; theorem :: JORDAN15:1 :: Uogolnic i przenisc cmp. JORDAN1A:15 for A,B be Subset of TOP-REAL 2 st A meets B holds proj1.:A meets proj1.:B; theorem :: JORDAN15:2 for A,B be Subset of TOP-REAL 2 for s be Real st A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s holds proj1.:A misses proj1.:B; theorem :: JORDAN15:3 for S be closed Subset of TOP-REAL 2 st S is bounded holds proj1 .:S is closed; theorem :: JORDAN15:4 for S be compact Subset of TOP-REAL 2 holds proj1.:S is compact; theorem :: JORDAN15:5 for G be Go-board for i,j,k,j1,k1 be Nat st 1 <= i & i <= len G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds LSeg(G*(i ,j1),G*(i,k1)) c= LSeg(G*(i,j),G*(i,k)); theorem :: JORDAN15:6 for G be Go-board for i,j,k,j1,k1 be Nat st 1 <= i & i <= width G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds LSeg(G*( j1,i),G*(k1,i)) c= LSeg(G*(j,i),G*(k,i)); theorem :: JORDAN15:7 for G be Go-board for j,k,j1,k1 be Nat st 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds LSeg(G*(Center G,j1),G*(Center G,k1)) c= LSeg(G*(Center G,j),G*(Center G,k)); theorem :: JORDAN15:8 for G be Go-board st len G = width G for j,k,j1,k1 be Nat st 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds LSeg(G*(j1,Center G ),G*(k1,Center G)) c= LSeg(G*(j,Center G),G*(k,Center G)); theorem :: JORDAN15:9 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) ex j1 be Nat st j <= j1 & j1 <= k & LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k )) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i,j1)}; theorem :: JORDAN15:10 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & Gauge(C,n)*(i,k) in L~Upper_Seq(C,n) ex k1 be Nat st j <= k1 & k1 <= k & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k1 )) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,k1)}; theorem :: JORDAN15:11 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) & Gauge (C,n)*(i,k) in L~Upper_Seq(C,n) ex j1,k1 be Nat st j <= j1 & j1 <= k1 & k1 <= k & LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i,j1)} & LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq( C,n) = {Gauge(C,n)*(i,k1)}; theorem :: JORDAN15:12 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= j & j <= k & k <= len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) ex j1 be Nat st j <= j1 & j1 <= k & LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k,i )) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(j1,i)}; theorem :: JORDAN15:13 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= j & j <= k & k <= len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*(k,i) in L~Upper_Seq(C,n) ex k1 be Nat st j <= k1 & k1 <= k & LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k1,i )) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(k1,i)}; theorem :: JORDAN15:14 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= j & j <= k & k <= len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) & Gauge (C,n)*(k,i) in L~Upper_Seq(C,n) ex j1,k1 be Nat st j <= j1 & j1 <= k1 & k1 <= k & LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(j1,i)} & LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq( C,n) = {Gauge(C,n)*(k1,i)}; theorem :: JORDAN15:15 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) ex j1 be Nat st j <= j1 & j1 <= k & LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k )) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,j1)}; theorem :: JORDAN15:16 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & Gauge(C,n)*(i,k) in L~Lower_Seq(C,n) ex k1 be Nat st j <= k1 & k1 <= k & LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k1 )) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(i,k1)}; theorem :: JORDAN15:17 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= i & i <= len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & Gauge(C,n)*(i,j) in L~Upper_Seq(C,n) & Gauge (C,n)*(i,k) in L~Lower_Seq(C,n) ex j1,k1 be Nat st j <= j1 & j1 <= k1 & k1 <= k & LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i,j1)} & LSeg(Gauge(C,n)*(i,j1),Gauge(C,n)*(i,k1)) /\ L~Lower_Seq( C,n) = {Gauge(C,n)*(i,k1)}; theorem :: JORDAN15:18 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= j & j <= k & k <= len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*(j,i) in L~Upper_Seq(C,n) ex j1 be Nat st j <= j1 & j1 <= k & LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k,i )) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(j1,i)}; theorem :: JORDAN15:19 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= j & j <= k & k <= len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*(k,i) in L~Lower_Seq(C,n) ex k1 be Nat st j <= k1 & k1 <= k & LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k1,i )) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(k1,i)}; theorem :: JORDAN15:20 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 <= j & j <= k & k <= len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*(j,i) in L~Upper_Seq(C,n) & Gauge (C,n)*(k,i) in L~Lower_Seq(C,n) ex j1,k1 be Nat st j <= j1 & j1 <= k1 & k1 <= k & LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(j1,i)} & LSeg(Gauge(C,n)*(j1,i),Gauge(C,n)*(k1,i)) /\ L~Lower_Seq( C,n) = {Gauge(C,n)*(k1,i)}; theorem :: JORDAN15:21 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & Gauge(C,n)*( i,k) in L~Upper_Seq(C,n) & Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) holds LSeg( Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C; theorem :: JORDAN15:22 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & Gauge(C,n)*( i,k) in L~Upper_Seq(C,n) & Gauge(C,n)*(i,j) in L~Lower_Seq(C,n) holds LSeg( Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C; theorem :: JORDAN15:23 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 & Gauge(C,n)*(i,k) in Upper_Arc L~Cage(C,n) & Gauge(C,n)*(i,j) in Lower_Arc L~ Cage(C,n) holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Lower_Arc C; theorem :: JORDAN15:24 for C be Simple_closed_curve for i,j,k be Nat st 1 < i & i < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C,n) & n > 0 & Gauge(C,n)*(i,k) in Upper_Arc L~Cage(C,n) & Gauge(C,n)*(i,j) in Lower_Arc L~ Cage(C,n) holds LSeg(Gauge(C,n)*(i,j),Gauge(C,n)*(i,k)) meets Upper_Arc C; theorem :: JORDAN15:25 for C be Simple_closed_curve for j,k be Nat holds 1 <= j & j <= k & k <= width Gauge(C,n+1) & Gauge(C,n+1)*(Center Gauge(C,n+1),k) in Upper_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~ Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*( Center Gauge(C,n+1),k)) meets Lower_Arc C; theorem :: JORDAN15:26 for C be Simple_closed_curve for j,k be Nat holds 1 <= j & j <= k & k <= width Gauge(C,n+1) & Gauge(C,n+1)*(Center Gauge(C,n+1),k) in Upper_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~ Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*( Center Gauge(C,n+1),k)) meets Upper_Arc C; theorem :: JORDAN15:27 for C be compact connected non vertical non horizontal Subset of TOP-REAL 2 for i,j,k be Nat st 1 < j & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*(k,i) in L~Upper_Seq(C,n) & Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) holds j <> k; theorem :: JORDAN15:28 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & LSeg(Gauge(C ,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(k,i)} & LSeg( Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(j,i)} holds LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C; theorem :: JORDAN15:29 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & LSeg(Gauge(C ,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(k,i)} & LSeg( Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(j,i)} holds LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C; theorem :: JORDAN15:30 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*( k,i) in L~Upper_Seq(C,n) & Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) holds LSeg( Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C; theorem :: JORDAN15:31 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*( k,i) in L~Upper_Seq(C,n) & Gauge(C,n)*(j,i) in L~Lower_Seq(C,n) holds LSeg( Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C; theorem :: JORDAN15:32 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & n > 0 & Gauge(C,n)*(k,i) in Upper_Arc L~Cage(C,n) & Gauge(C,n)*(j,i) in Lower_Arc L~ Cage(C,n) holds LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C; theorem :: JORDAN15:33 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & n > 0 & Gauge(C,n)*(k,i) in Upper_Arc L~Cage(C,n) & Gauge(C,n)*(j,i) in Lower_Arc L~ Cage(C,n) holds LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C; theorem :: JORDAN15:34 for C be Simple_closed_curve for j,k be Nat holds 1 < j & j <= k & k < len Gauge(C,n+1) & Gauge(C,n+1)*(k,Center Gauge(C,n+1)) in Upper_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(j,Center Gauge(C,n+1)) in Lower_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(j,Center Gauge(C,n+1)), Gauge(C,n+1)*(k,Center Gauge (C,n+1))) meets Lower_Arc C; theorem :: JORDAN15:35 for C be Simple_closed_curve for j,k be Nat holds 1 < j & j <= k & k < len Gauge(C,n+1) & Gauge(C,n+1)*(k,Center Gauge(C,n+1)) in Upper_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(j,Center Gauge(C,n+1)) in Lower_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(j,Center Gauge(C,n+1)), Gauge(C,n+1)*(k,Center Gauge (C,n+1))) meets Upper_Arc C; theorem :: JORDAN15:36 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & LSeg(Gauge(C ,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(j,i)} & LSeg( Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(k,i)} holds LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C; theorem :: JORDAN15:37 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & LSeg(Gauge(C ,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(j,i)} & LSeg( Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) /\ L~Lower_Seq(C,n) = {Gauge(C,n)*(k,i)} holds LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C; theorem :: JORDAN15:38 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*( j,i) in L~Upper_Seq(C,n) & Gauge(C,n)*(k,i) in L~Lower_Seq(C,n) holds LSeg( Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C; theorem :: JORDAN15:39 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & Gauge(C,n)*( j,i) in L~Upper_Seq(C,n) & Gauge(C,n)*(k,i) in L~Lower_Seq(C,n) holds LSeg( Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C; theorem :: JORDAN15:40 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & n > 0 & Gauge(C,n)*(j,i) in Upper_Arc L~Cage(C,n) & Gauge(C,n)*(k,i) in Lower_Arc L~ Cage(C,n) holds LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Lower_Arc C; theorem :: JORDAN15:41 for C be Simple_closed_curve for i,j,k be Nat st 1 < j & j <= k & k < len Gauge(C,n) & 1 <= i & i <= width Gauge(C,n) & n > 0 & Gauge(C,n)*(j,i) in Upper_Arc L~Cage(C,n) & Gauge(C,n)*(k,i) in Lower_Arc L~ Cage(C,n) holds LSeg(Gauge(C,n)*(j,i),Gauge(C,n)*(k,i)) meets Upper_Arc C; theorem :: JORDAN15:42 for C be Simple_closed_curve for j,k be Nat holds 1 < j & j <= k & k < len Gauge(C,n+1) & Gauge(C,n+1)*(j,Center Gauge(C,n+1)) in Upper_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(k,Center Gauge(C,n+1)) in Lower_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(j,Center Gauge(C,n+1)), Gauge(C,n+1)*(k,Center Gauge (C,n+1))) meets Lower_Arc C; theorem :: JORDAN15:43 for C be Simple_closed_curve for j,k be Nat holds 1 < j & j <= k & k < len Gauge(C,n+1) & Gauge(C,n+1)*(j,Center Gauge(C,n+1)) in Upper_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(k,Center Gauge(C,n+1)) in Lower_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(j,Center Gauge(C,n+1)), Gauge(C,n+1)*(k,Center Gauge (C,n+1))) meets Upper_Arc C; theorem :: JORDAN15:44 for C be Simple_closed_curve for i1,i2,j,k be Nat st 1 < i1 & i1 <= i2 & i2 < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C, n) & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge (C,n)*(i2,k))) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i2,k)} & (LSeg(Gauge(C,n)*(i1 ,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~ Lower_Seq(C,n) = {Gauge(C,n)*(i1,j)} holds (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*( i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Upper_Arc C; theorem :: JORDAN15:45 for C be Simple_closed_curve for i1,i2,j,k be Nat st 1 < i1 & i1 <= i2 & i2 < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C, n) & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge (C,n)*(i2,k))) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i2,k)} & (LSeg(Gauge(C,n)*(i1 ,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~ Lower_Seq(C,n) = {Gauge(C,n)*(i1,j)} holds (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*( i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Lower_Arc C; theorem :: JORDAN15:46 for C be Simple_closed_curve for i1,i2,j,k be Nat st 1 < i2 & i2 <= i1 & i1 < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C, n) & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge (C,n)*(i2,k))) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i2,k)} & (LSeg(Gauge(C,n)*(i1 ,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~ Lower_Seq(C,n) = {Gauge(C,n)*(i1,j)} holds (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*( i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Upper_Arc C; theorem :: JORDAN15:47 for C be Simple_closed_curve for i1,i2,j,k be Nat st 1 < i2 & i2 <= i1 & i1 < len Gauge(C,n) & 1 <= j & j <= k & k <= width Gauge(C, n) & (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge (C,n)*(i2,k))) /\ L~Upper_Seq(C,n) = {Gauge(C,n)*(i2,k)} & (LSeg(Gauge(C,n)*(i1 ,j),Gauge(C,n)*(i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) /\ L~ Lower_Seq(C,n) = {Gauge(C,n)*(i1,j)} holds (LSeg(Gauge(C,n)*(i1,j),Gauge(C,n)*( i1,k)) \/ LSeg(Gauge(C,n)*(i1,k),Gauge(C,n)*(i2,k))) meets Lower_Arc C; theorem :: JORDAN15:48 for C be Simple_closed_curve for i1,i2,j,k be Nat holds 1 < i1 & i1 < len Gauge(C,n+1) & 1 < i2 & i2 < len Gauge(C,n+1) & 1 <= j & j <= k & k <= width Gauge(C,n+1) & Gauge(C,n+1)*(i1,k) in Upper_Arc L~Cage(C, n+1) & Gauge(C,n+1)*(i2,j) in Lower_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1) *(i2,j),Gauge(C,n+1)*(i2,k)) \/ LSeg(Gauge(C,n+1)*(i2,k),Gauge(C,n+1)*(i1,k)) meets Upper_Arc C; theorem :: JORDAN15:49 for C be Simple_closed_curve for i1,i2,j,k be Nat holds 1 < i1 & i1 < len Gauge(C,n+1) & 1 < i2 & i2 < len Gauge(C,n+1) & 1 <= j & j <= k & k <= width Gauge(C,n+1) & Gauge(C,n+1)*(i1,k) in Upper_Arc L~Cage(C, n+1) & Gauge(C,n+1)*(i2,j) in Lower_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1) *(i2,j),Gauge(C,n+1)*(i2,k)) \/ LSeg(Gauge(C,n+1)*(i2,k),Gauge(C,n+1)*(i1,k)) meets Lower_Arc C; theorem :: JORDAN15:50 for C be Simple_closed_curve for i,j,k be Nat holds 1 < i & i < len Gauge(C,n+1) & 1 <= j & j <= k & k <= width Gauge(C,n+1) & Gauge(C,n+1) *(i,k) in Upper_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) \/ LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1) ,k),Gauge(C,n+1)*(i,k)) meets Upper_Arc C; theorem :: JORDAN15:51 for C be Simple_closed_curve for i,j,k be Nat holds 1 < i & i < len Gauge(C,n+1) & 1 <= j & j <= k & k <= width Gauge(C,n+1) & Gauge(C,n+1) *(i,k) in Upper_Arc L~Cage(C,n+1) & Gauge(C,n+1)*(Center Gauge(C,n+1),j) in Lower_Arc L~Cage(C,n+1) implies LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1),j), Gauge(C,n+1)*(Center Gauge(C,n+1),k)) \/ LSeg(Gauge(C,n+1)*(Center Gauge(C,n+1) ,k),Gauge(C,n+1)*(i,k)) meets Lower_Arc C;