let C be Simple_closed_curve; :: thesis: 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
let i, j be 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
A3: (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 = (LMP (L~ (Cage (C,i)))) `2 by A1, Th22;
(LMP (Lower_Arc (L~ (Cage (C,j))))) `2 = (LMP (L~ (Cage (C,j)))) `2 by A1, A2, Th22;
hence (LMP (Lower_Arc (L~ (Cage (C,i))))) `2 <= (LMP (Lower_Arc (L~ (Cage (C,j))))) `2 by A2, A3, Th26; :: thesis: verum