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
for
p being
Point of 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 = sup (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 )