theorem Th27: :: JORDAN22:27

for C being Simple_closed_curve
for i, j being Nat st 0 < i & i <= j holds
(UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2