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:11;
A6: Center (Gauge (C,(n + 1))) <= len (Gauge (C,(n + 1))) by JORDAN1B:13;
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:61;
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