let n be 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 Upper_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 Upper_Arc C
A1: 4 <= len (Gauge (C,n)) by JORDAN8:10;
then len (Gauge (C,n)) >= 2 by XXREAL_0:2;
then A2: 1 < Center (Gauge (C,n)) by Th14;
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 Upper_Arc C by A2, Th15, Th25; :: thesis: verum