theorem Th23: :: JORDAN22:23

for C being Simple_closed_curve
for n being Nat st 0 < n holds
(UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2