let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for j being 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 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 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 and
A3: 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)));
A4: 1 <= Center (Gauge (C,(n + 1))) by JORDAN1B:11;
A5: Upper_Arc (L~ (Cage (C,(n + 1)))) c= L~ (Cage (C,(n + 1))) by JORDAN6:61;
A6: Center (Gauge (C,(n + 1))) <= len (Gauge (C,(n + 1))) by JORDAN1B:13;
n + 1 >= 0 + 1 by NAT_1:11;
then 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:45;
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, A3, A4, A6, A5, JORDAN1G:57, XBOOLE_1:63; :: thesis: verum