begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
begin
theorem
theorem Th7:
theorem
theorem
theorem
begin
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem
theorem
theorem
theorem
for
i,
k being
Element of
NAT for
C being non
empty being_simple_closed_curve compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
p being
Point of
(TOP-REAL 2) st
p `1 = ((W-bound C) + (E-bound C)) / 2 &
i > 0 & 1
<= k &
k <= width (Gauge (C,i)) &
(Gauge (C,i)) * (
(Center (Gauge (C,i))),
k)
in Upper_Arc (L~ (Cage (C,i))) &
p `2 = upper_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (Lower_Arc (L~ (Cage (C,i)))))) holds
ex
j being
Element of
NAT st
( 1
<= j &
j <= width (Gauge (C,i)) &
p = (Gauge (C,i)) * (
(Center (Gauge (C,i))),
j) )