let n be Element of NAT ; :: thesis: for C being Simple_closed_curve
for j, k being Element of NAT st 1 < j & j <= k & k < len (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Lower_Arc C
let C be Simple_closed_curve; :: thesis: for j, k being Element of NAT st 1 < j & j <= k & k < len (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Lower_Arc C
let j, k be Element of NAT ; :: thesis: ( 1 < j & j <= k & k < len (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) implies LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Lower_Arc C )
assume that
A1: 1 < j and
A2: j <= k and
A3: k < len (Gauge C,(n + 1)) and
A4: (Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) and
A5: (Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) ; :: thesis: LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Lower_Arc C
A6: len (Gauge C,(n + 1)) >= 4 by JORDAN8:13;
then len (Gauge C,(n + 1)) >= 3 by XXREAL_0:2;
then Center (Gauge C,(n + 1)) < len (Gauge C,(n + 1)) by JORDAN1B:16;
then A7: Center (Gauge C,(n + 1)) < width (Gauge C,(n + 1)) by JORDAN8:def 1;
len (Gauge C,(n + 1)) >= 2 by A6, XXREAL_0:2;
then 1 < Center (Gauge C,(n + 1)) by JORDAN1B:15;
hence LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Lower_Arc C by A1, A2, A3, A4, A5, A7, Th34; :: thesis: verum