theorem Th18: :: JORDAN22:18

for C being Simple_closed_curve
for n being Nat holds (LMP C) `2 > (LMP (L~ (Cage (C,n)))) `2