begin
theorem
theorem
theorem Th3:
theorem Th4:
theorem
canceled;
theorem
canceled;
theorem Th7:
for
G being
Go-board for
i,
j,
k,
j1,
k1 being
Element of
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 Th8:
for
G being
Go-board for
i,
j,
k,
j1,
k1 being
Element of
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
theorem
theorem Th11:
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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 Th13:
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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 Th15:
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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 Th16:
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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 Th20:
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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 Th22:
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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
Element of
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 Th23:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th24:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th25:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th26:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
Element of
NAT for
C being
Simple_closed_curve for
j,
k being
Element of
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
Element of
NAT for
C being
Simple_closed_curve for
j,
k being
Element of
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 Th29:
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j,
k being
Element of
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 Th30:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th31:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th32:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th33:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th34:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th35:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
Element of
NAT for
C being
Simple_closed_curve for
j,
k being
Element of
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
Element of
NAT for
C being
Simple_closed_curve for
j,
k being
Element of
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 Th38:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th39:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th40:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th41:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th42:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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 Th43:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
Element of
NAT for
C being
Simple_closed_curve for
j,
k being
Element of
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
Element of
NAT for
C being
Simple_closed_curve for
j,
k being
Element of
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 Th46:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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 Th47:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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 Th48:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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 Th49:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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 Th50:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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 Th51:
for
n being
Element of
NAT for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Element of
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
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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
Element of
NAT for
C being
Simple_closed_curve for
i,
j,
k being
Element of
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