theorem Th26: :: JORDAN22:26

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