for C being Simple_closed_curve
for n being Nat st 0 < n holds
LMP (L~ (Cage (C,n))) = |[(((E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n))))) / 2),(lower_bound (proj2 .: ((L~ (Cage (C,n))) /\ (LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n))))))))))]| by Th14;