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