theorem :: JORDAN1A:38

for i being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,1)) holds
((Gauge (C,1)) * ((Center (Gauge (C,1))),i)) `1 = ((W-bound C) + (E-bound C)) / 2