environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, XBOOLE_0;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2, TARSKI, JORDAN3, PSCOMP_1, FINSEQ_5, FINSEQ_6, GOBOARD7, TOPREAL1, GOBOARD5, SPRECT_2, SPPOL_1, FUNCT_2, GOBOARD9, FINSEQ_2, SUBSET_1, JORDAN4, SPRECT_3, TOPREAL3, JORDAN8, PARTFUN2, SPRECT_1, XBOOLE_0, XBOOLE_1, ZFMISC_1, SEQ_4, GOBRD14, TOPREAL6, JORDAN2C, PRE_TOPC, JORDAN6, JORDAN9, JORDAN1H, JORDAN1A, JORDAN1C, JORDAN1E, JORDAN10, JGRAPH_1, REVROT_1, RCOMP_1, COMPTS_1, ENUMSET1, JORDAN1B, JORDAN1F, JORDAN1G, JORDAN1I, JORDAN1J, GOBOARD3, TOPREAL8, GRAPH_2, SPRECT_5, JORDAN1D, XREAL_1, XXREAL_0, JCT_MISC, PARTFUN1, MATRIX_0, XXREAL_2, NAT_D, XREAL_0, RLTOPSP1;
schemes ;
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;
constructors HIDDEN, 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;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities PSCOMP_1;
expansions TARSKI, XBOOLE_0;
theorem Th5:
for
G being
Go-board for
i,
j,
k,
j1,
k1 being
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 Th6:
for
G being
Go-board for
i,
j,
k,
j1,
k1 being
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 Th9:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
j1 being
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
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
k1 being
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 Th11:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
j1,
k1 being
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
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
j1 being
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 Th13:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
k1 being
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 Th14:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
j1,
k1 being
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
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
j1 being
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
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
k1 being
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
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
j1,
k1 being
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 Th18:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
j1 being
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
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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)) holds
ex
k1 being
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 Th20:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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
ex
j1,
k1 being
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 Th21:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th22:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th23:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th24:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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
for
n being
Nat for
C being
Simple_closed_curve for
j,
k being
Nat st 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)))) holds
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
for
n being
Nat for
C being
Simple_closed_curve for
j,
k being
Nat st 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)))) holds
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 Th27:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
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 Th28:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th29:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th30:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th31:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th32:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th33:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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
for
n being
Nat for
C being
Simple_closed_curve for
j,
k being
Nat st 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)))) holds
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
for
n being
Nat for
C being
Simple_closed_curve for
j,
k being
Nat st 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)))) holds
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 Th36:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th37:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th38:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th39:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th40:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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 Th41:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
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
for
n being
Nat for
C being
Simple_closed_curve for
j,
k being
Nat st 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)))) holds
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
for
n being
Nat for
C being
Simple_closed_curve for
j,
k being
Nat st 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)))) holds
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 Th44:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
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 Th45:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
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 Th46:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
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 Th47:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
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 Th48:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Nat st 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)))) holds
(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 Th49:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Nat st 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)))) holds
(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
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 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)))) holds
(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
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 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)))) holds
(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