let C be Simple_closed_curve; :: thesis: for i, j being Nat st 0 < i & i <= j holds
(UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2
let i, j be Nat; :: thesis: ( 0 < i & i <= j implies (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 )
assume that
A1: 0 < i and
A2: i <= j ; :: thesis: (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2
A3: (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 = (UMP (L~ (Cage (C,i)))) `2 by A1, Th21;
(UMP (Upper_Arc (L~ (Cage (C,j))))) `2 = (UMP (L~ (Cage (C,j)))) `2 by A1, A2, Th21;
hence (UMP (Upper_Arc (L~ (Cage (C,j))))) `2 <= (UMP (Upper_Arc (L~ (Cage (C,i))))) `2 by A2, A3, Th25; :: thesis: verum