theorem Th27: :: JORDAN14:27

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n, m being Nat st m >= n & n >= 1 holds
X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2