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