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