theorem
for
i,
j,
m,
n being
Nat for
D being non
empty Subset of
(TOP-REAL 2) st 1
<= i &
i <= len (Gauge (D,n)) & 1
<= j &
j <= len (Gauge (D,m)) & ( (
n > 0 &
m > 0 ) or (
n = 0 &
m = 0 ) ) holds
((Gauge (D,n)) * (i,(Center (Gauge (D,n))))) `2 = ((Gauge (D,m)) * (j,(Center (Gauge (D,m))))) `2