let C be Simple_closed_curve; :: thesis: for i, j being Element of NAT st 0 < i & i <= j holds
(LMP (Lower_Arc (L~ (Cage C,i)))) `2 <= (LMP (Lower_Arc (L~ (Cage C,j)))) `2
let i, j be Element of NAT ; :: thesis: ( 0 < i & i <= j implies (LMP (Lower_Arc (L~ (Cage C,i)))) `2 <= (LMP (Lower_Arc (L~ (Cage C,j)))) `2 )
assume that
A1: 0 < i and
A2: i <= j ; :: thesis: (LMP (Lower_Arc (L~ (Cage C,i)))) `2 <= (LMP (Lower_Arc (L~ (Cage C,j)))) `2
( (LMP (Lower_Arc (L~ (Cage C,i)))) `2 = (LMP (L~ (Cage C,i))) `2 & (LMP (Lower_Arc (L~ (Cage C,j)))) `2 = (LMP (L~ (Cage C,j))) `2 ) by A1, A2, Th24;
hence (LMP (Lower_Arc (L~ (Cage C,i)))) `2 <= (LMP (Lower_Arc (L~ (Cage C,j)))) `2 by A2, Th28; :: thesis: verum