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 <= width (Gauge C,(n + 1)) & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} holds
LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Lower_Arc C
let C be Simple_closed_curve; :: thesis: for j, k being Element of NAT st 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} holds
LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Lower_Arc C
let j, k be Element of NAT ; :: thesis: ( 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} implies LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Lower_Arc C )
assume that
A1: ( 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) ) and
A2: (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} and
A3: (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} ; :: thesis: LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Lower_Arc C
A4: len (Gauge C,(n + 1)) >= 4 by JORDAN8:13;
then A5: len (Gauge C,(n + 1)) >= 3 by XXREAL_0:2;
len (Gauge C,(n + 1)) >= 2 by A4, 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) meets Lower_Arc C by A1, A2, A3, A5, Th60, JORDAN1B:16; :: thesis: verum