theorem Th28: :: JORDAN22:28

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