let n be Nat; for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (k,i) in Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (j,i) in Lower_Arc (L~ (Cage (C,n))) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
let C be Simple_closed_curve; for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (k,i) in Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (j,i) in Lower_Arc (L~ (Cage (C,n))) holds
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
let i, j, k be Nat; ( 1 < j & j <= k & k < len (Gauge (C,n)) & 1 <= i & i <= width (Gauge (C,n)) & n > 0 & (Gauge (C,n)) * (k,i) in Upper_Arc (L~ (Cage (C,n))) & (Gauge (C,n)) * (j,i) in Lower_Arc (L~ (Cage (C,n))) implies LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C )
assume that
A1:
1 < j
and
A2:
j <= k
and
A3:
k < len (Gauge (C,n))
and
A4:
1 <= i
and
A5:
i <= width (Gauge (C,n))
and
A6:
n > 0
and
A7:
(Gauge (C,n)) * (k,i) in Upper_Arc (L~ (Cage (C,n)))
and
A8:
(Gauge (C,n)) * (j,i) in Lower_Arc (L~ (Cage (C,n)))
; LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
A9:
L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n)))
by A6, JORDAN1G:56;
L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n)))
by A6, JORDAN1G:55;
hence
LSeg (((Gauge (C,n)) * (j,i)),((Gauge (C,n)) * (k,i))) meets Upper_Arc C
by A1, A2, A3, A4, A5, A7, A8, A9, Th31; verum