begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem
theorem Th7:
theorem
theorem
theorem
theorem
theorem Th12:
theorem
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem
theorem
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
for
G being
Go-board for
f being
S-Sequence_in_R2 for
p being
Point of
(TOP-REAL 2) for
k being
Element of
NAT st 1
<= k &
k < p .. f &
f is_sequence_on G &
p in rng f holds
(
left_cell (R_Cut f,p),
k,
G = left_cell f,
k,
G &
right_cell (R_Cut f,p),
k,
G = right_cell f,
k,
G )
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
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 &
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
j <> k
theorem Th58:
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) &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k)} &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Lower_Arc C
theorem Th59:
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) &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k)} &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Upper_Arc C
theorem Th60:
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 &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),
((Gauge C,n) * i,k) meets Lower_Arc C
theorem Th61:
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 &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} &
(LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} 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
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
j being
Element of
NAT st
(Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),
j in Upper_Arc (L~ (Cage C,(n + 1))) & 1
<= j &
j <= width (Gauge C,(n + 1)) holds
LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),
((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Lower_Arc (L~ (Cage C,(n + 1)))
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)) &
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} &
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} 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)) &
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} &
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} 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
theorem
theorem
theorem