for C being Simple_closed_curve
for n being Nat st 0 < n holds
ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & LMP (L~ (Cage (C,n))) = (Gauge (C,n)) * ((Center (Gauge (C,n))),i) )