let n be Element of NAT ; :: thesis: for C being Simple_closed_curve holds LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets Lower_Arc C
let C be Simple_closed_curve; :: thesis: LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets Lower_Arc C
A1: 4 <= len (Gauge C,n) by JORDAN8:13;
then len (Gauge C,n) >= 2 by XXREAL_0:2;
then A2: 1 < Center (Gauge C,n) by Th15;
len (Gauge C,n) >= 3 by A1, XXREAL_0:2;
hence LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets Lower_Arc C by A2, Th16, Th29; :: thesis: verum