let C be Simple_closed_curve; :: thesis: for n being Element of NAT st 0 < n holds
(UMP C) `2 < (UMP (Upper_Arc (L~ (Cage C,n)))) `2
let n be Element of NAT ; :: thesis: ( 0 < n implies (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage C,n)))) `2 )
assume 0 < n ; :: thesis: (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage C,n)))) `2
then UMP (Upper_Arc (L~ (Cage C,n))) = UMP (L~ (Cage C,n)) by Th23;
hence (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage C,n)))) `2 by Th17; :: thesis: verum