theorem Th25: :: JORDAN22:25

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