theorem Th46:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) 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 L~ (Lower_Seq (C,n))