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 Lower_Arc (L~ (Cage C,(n + 1))) & 1 <= j & j <= width (Gauge C,(n + 1)) holds
LSeg ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Upper_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 Lower_Arc (L~ (Cage C,(n + 1))) & 1 <= j & j <= width (Gauge C,(n + 1)) holds
LSeg ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Upper_Arc (L~ (Cage C,(n + 1)))
let j be Element of NAT ; :: thesis: ( (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Lower_Arc (L~ (Cage C,(n + 1))) & 1 <= j & j <= width (Gauge C,(n + 1)) implies LSeg ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Upper_Arc (L~ (Cage C,(n + 1))) )
assume that
A1: (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Lower_Arc (L~ (Cage C,(n + 1))) and
A2: 1 <= j and
A3: j <= width (Gauge C,(n + 1)) ; :: thesis: LSeg ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Upper_Arc (L~ (Cage C,(n + 1)))
set in1 = Center (Gauge C,(n + 1));
A4: n + 1 >= 0 + 1 by NAT_1:11;
A5: 1 <= Center (Gauge C,(n + 1)) by JORDAN1B:12;
A6: Center (Gauge C,(n + 1)) <= len (Gauge C,(n + 1)) by JORDAN1B:14;
A7: LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),(width (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) c= LSeg ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) by A2, A3, A4, Th2;
Lower_Arc (L~ (Cage C,(n + 1))) c= L~ (Cage C,(n + 1)) by JORDAN6:76;
hence LSeg ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Upper_Arc (L~ (Cage C,(n + 1))) by A1, A2, A3, A5, A6, A7, Th4, XBOOLE_1:63; :: thesis: verum