theorem
for
j,
m,
n being
Nat for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) st 1
<= m &
m <= n & 1
<= j &
j <= width (Gauge (E,n)) holds
LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))
c= LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),
((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))