let C be Simple_closed_curve; :: thesis: for i, j being Element of 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 Element of 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
( (UMP (Upper_Arc (L~ (Cage C,i)))) `2 = (UMP (L~ (Cage C,i))) `2 & (UMP (Upper_Arc (L~ (Cage C,j)))) `2 = (UMP (L~ (Cage C,j))) `2 ) by A1, A2, Th23;
hence (UMP (Upper_Arc (L~ (Cage C,j)))) `2 <= (UMP (Upper_Arc (L~ (Cage C,i)))) `2 by A2, Th27; :: thesis: verum