let n be Element of NAT ; :: thesis: for C being Simple_closed_curve
for i, j, k being Element of 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 Upper_Arc C
let C be Simple_closed_curve; :: thesis: for i, j, k being Element of 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 Upper_Arc C
let i, j, k be Element of 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 Upper_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 Upper_Arc C
A8: len (Gauge C,(n + 1)) >= 4 by JORDAN8:13;
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:16;
len (Gauge C,(n + 1)) >= 2 by A8, XXREAL_0:2;
then 1 < Center (Gauge C,(n + 1)) by JORDAN1B:15;
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 Upper_Arc C by A1, A2, A3, A4, A5, A6, A7, A9, Th50; :: thesis: verum