let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for n being Nat st n > 0 holds
for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets Upper_Arc (L~ (Cage (C,n)))
let n be Nat; ( n > 0 implies for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets Upper_Arc (L~ (Cage (C,n))) )
assume A1:
n > 0
; for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets Upper_Arc (L~ (Cage (C,n)))
let i, j be Nat; ( 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) implies LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets Upper_Arc (L~ (Cage (C,n))) )
assume that
A2:
1 <= i
and
A3:
i <= len (Gauge (C,n))
and
A4:
1 <= j
and
A5:
j <= width (Gauge (C,n))
and
A6:
(Gauge (C,n)) * (i,j) in L~ (Cage (C,n))
; LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets Upper_Arc (L~ (Cage (C,n)))
L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n)))
by A1, JORDAN1G:55;
hence
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets Upper_Arc (L~ (Cage (C,n)))
by A2, A3, A4, A5, A6, Th3; verum