theorem Th17: :: JORDAN22:17
for C being Simple_closed_curve
for n being Nat holds (UMP C) `2 < (UMP (L~ (Cage (C,n)))) `2