let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets Lower_Arc (L~ (Cage C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets Lower_Arc (L~ (Cage C,n))
A1: 4 <= len (Gauge C,n) by JORDAN8:13;
then len (Gauge C,n) >= 3 by XXREAL_0:2;
then A2: Center (Gauge C,n) < len (Gauge C,n) by Th16;
len (Gauge C,n) >= 2 by A1, XXREAL_0:2;
then 1 < Center (Gauge C,n) by Th15;
hence LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets Lower_Arc (L~ (Cage C,n)) by A2, Th33; :: thesis: verum