let n be Nat; 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; 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: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 Lower_Arc C
by A2, Th15, Th26; verum