let C be Simple_closed_curve; 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; ( 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
; (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; verum