let n be 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 Upper_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 Upper_Arc (L~ (Cage (C,n)))

A1: 4 <= len (Gauge (C,n)) by JORDAN8:10;

then len (Gauge (C,n)) >= 3 by XXREAL_0:2;

then A2: Center (Gauge (C,n)) < len (Gauge (C,n)) by Th15;

len (Gauge (C,n)) >= 2 by A1, XXREAL_0:2;

then 1 < Center (Gauge (C,n)) by Th14;

hence LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by A2, Th29; :: thesis: verum

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 Upper_Arc (L~ (Cage (C,n)))

A1: 4 <= len (Gauge (C,n)) by JORDAN8:10;

then len (Gauge (C,n)) >= 3 by XXREAL_0:2;

then A2: Center (Gauge (C,n)) < len (Gauge (C,n)) by Th15;

len (Gauge (C,n)) >= 2 by A1, XXREAL_0:2;

then 1 < Center (Gauge (C,n)) by Th14;

hence LSeg (((Gauge (C,n)) * ((Center (Gauge (C,n))),1)),((Gauge (C,n)) * ((Center (Gauge (C,n))),(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by A2, Th29; :: thesis: verum