let n be Nat; :: thesis: for C being Simple_closed_curve

for j, k being 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 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 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:10;

then len (Gauge (C,(n + 1))) >= 3 by XXREAL_0:2;

then Center (Gauge (C,(n + 1))) < len (Gauge (C,(n + 1))) by JORDAN1B:15;

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:14;

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, Th32; :: thesis: verum

for j, k being 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 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 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:10;

then len (Gauge (C,(n + 1))) >= 3 by XXREAL_0:2;

then Center (Gauge (C,(n + 1))) < len (Gauge (C,(n + 1))) by JORDAN1B:15;

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:14;

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, Th32; :: thesis: verum