theorem
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat st
n > 0 holds
for
i,
j being
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)))