let n be Nat; 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 Upper_Arc C
let C be 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 Upper_Arc C
let i, j, k be Nat; ( 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 Upper_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))
; LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_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 Upper_Arc C
by A1, A2, A9, A11, A12, A13, JORDAN1J:59;
hence
LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k))) meets Upper_Arc C
by A1, A2, A3, A5, A8, A9, A10, Th5, XBOOLE_1:63; verum