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 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 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 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

for j being 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 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 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