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