begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th16:
theorem
theorem Th18:
theorem
theorem Th20:
theorem
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem Th41:
theorem
theorem Th43:
theorem
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem Th54:
for
n being
Element of
NAT for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j being
Element of
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 Th55:
theorem Th56:
theorem Th57:
theorem Th58:
for
f being
S-Sequence_in_R2 for
Q being
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 Th59:
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
for
k being
Element of
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 Th60:
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
for
k being
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 Th61:
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
for
q being
Point of
(TOP-REAL 2) st
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))) holds
q `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
theorem Th62:
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
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 Th63:
theorem Th64:
theorem
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Element of
NAT st
n > 0 holds
for
i,
j being
Element of
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))