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 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (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 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

let i, j, k be Nat; :: thesis: ( 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) implies LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C )

assume that

A1: 1 < i and

A2: i < len (Gauge (C,n)) and

A3: 1 <= j and

A4: j <= k and

A5: k <= width (Gauge (C,n)) and

A6: (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) and

A7: (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) ; :: thesis: LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

consider j1, k1 being Nat such that

A8: j <= j1 and

A9: j1 <= k1 and

A10: k1 <= k and

A11: (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} and

A12: (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} by A1, A2, A3, A4, A5, A6, A7, Th11;

A13: k1 <= width (Gauge (C,n)) by A5, A10, XXREAL_0:2;

1 <= j1 by A3, A8, XXREAL_0:2;

then LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1))) meets Lower_Arc C by A1, A2, A9, A11, A12, A13, JORDAN1J:58;

hence LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C by A1, A2, A3, A5, A8, A9, A10, Th5, XBOOLE_1:63; :: thesis: verum

for i, j, k being Nat st 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (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 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) holds

LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

let i, j, k be Nat; :: thesis: ( 1 < i & i < len (Gauge (C,n)) & 1 <= j & j <= k & k <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) implies LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C )

assume that

A1: 1 < i and

A2: i < len (Gauge (C,n)) and

A3: 1 <= j and

A4: j <= k and

A5: k <= width (Gauge (C,n)) and

A6: (Gauge (C,n)) * (i,k) in L~ (Upper_Seq (C,n)) and

A7: (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) ; :: thesis: LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C

consider j1, k1 being Nat such that

A8: j <= j1 and

A9: j1 <= k1 and

A10: k1 <= k and

A11: (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j1))} and

A12: (LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k1))} by A1, A2, A3, A4, A5, A6, A7, Th11;

A13: k1 <= width (Gauge (C,n)) by A5, A10, XXREAL_0:2;

1 <= j1 by A3, A8, XXREAL_0:2;

then LSeg (((Gauge (C,n)) * (i,j1)),((Gauge (C,n)) * (i,k1))) meets Lower_Arc C by A1, A2, A9, A11, A12, A13, JORDAN1J:58;

hence LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Lower_Arc C by A1, A2, A3, A5, A8, A9, A10, Th5, XBOOLE_1:63; :: thesis: verum