let n be Nat; :: thesis: for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) \/ (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)),((Gauge (C,(n + 1))) * (i,k)))) meets Lower_Arc C
let C be Simple_closed_curve; :: thesis: for i, j, k being Nat st 1 < i & i < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) \/ (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)),((Gauge (C,(n + 1))) * (i,k)))) meets Lower_Arc C
let i, j, k be Nat; :: thesis: ( 1 < i & i < len (Gauge (C,(n + 1))) & 1 <= j & j <= k & k <= width (Gauge (C,(n + 1))) & (Gauge (C,(n + 1))) * (i,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) & (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) implies (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) \/ (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)),((Gauge (C,(n + 1))) * (i,k)))) meets Lower_Arc C )
assume that
A1: 1 < i and
A2: i < len (Gauge (C,(n + 1))) and
A3: 1 <= j and
A4: j <= k and
A5: k <= width (Gauge (C,(n + 1))) and
A6: (Gauge (C,(n + 1))) * (i,k) in Upper_Arc (L~ (Cage (C,(n + 1)))) and
A7: (Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j) in Lower_Arc (L~ (Cage (C,(n + 1)))) ; :: thesis: (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) \/ (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)),((Gauge (C,(n + 1))) * (i,k)))) meets Lower_Arc C
A8: len (Gauge (C,(n + 1))) >= 4 by JORDAN8:10;
then len (Gauge (C,(n + 1))) >= 3 by XXREAL_0:2;
then A9: Center (Gauge (C,(n + 1))) < len (Gauge (C,(n + 1))) by JORDAN1B:15;
len (Gauge (C,(n + 1))) >= 2 by A8, XXREAL_0:2;
then 1 < Center (Gauge (C,(n + 1))) by JORDAN1B:14;
hence (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)),((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)))) \/ (LSeg (((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),k)),((Gauge (C,(n + 1))) * (i,k)))) meets Lower_Arc C by A1, A2, A3, A4, A5, A6, A7, A9, Th49; :: thesis: verum