let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j being Element of NAT st (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Upper_Arc (L~ (Cage C,(n + 1))) & 1 <= j & j <= width (Gauge C,(n + 1)) holds
LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Lower_Arc (L~ (Cage C,(n + 1)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for j being Element of NAT st (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Upper_Arc (L~ (Cage C,(n + 1))) & 1 <= j & j <= width (Gauge C,(n + 1)) holds
LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Lower_Arc (L~ (Cage C,(n + 1)))
let j be Element of NAT ; :: thesis: ( (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Upper_Arc (L~ (Cage C,(n + 1))) & 1 <= j & j <= width (Gauge C,(n + 1)) implies LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Lower_Arc (L~ (Cage C,(n + 1))) )
assume that
A1: (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Upper_Arc (L~ (Cage C,(n + 1))) and
A2: ( 1 <= j & j <= width (Gauge C,(n + 1)) ) ; :: thesis: LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Lower_Arc (L~ (Cage C,(n + 1)))
set in1 = Center (Gauge C,(n + 1));
A3: n + 1 >= 0 + 1 by NAT_1:11;
A4: 1 <= Center (Gauge C,(n + 1)) by JORDAN1B:12;
A5: Center (Gauge C,(n + 1)) <= len (Gauge C,(n + 1)) by JORDAN1B:14;
A6: LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),1),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) c= LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) by A2, A3, JORDAN1A:66;
Upper_Arc (L~ (Cage C,(n + 1))) c= L~ (Cage C,(n + 1)) by JORDAN6:76;
hence LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Lower_Arc (L~ (Cage C,(n + 1))) by A1, A2, A4, A5, A6, JORDAN1G:65, XBOOLE_1:63; :: thesis: verum