let C be Simple_closed_curve; :: thesis: for n being Nat st 0 < n holds
(UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2
let n be 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 Th21;
hence (UMP C) `2 < (UMP (Upper_Arc (L~ (Cage (C,n))))) `2 by Th17; :: thesis: verum