let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT st n > 0 holds
for i, j being Element of 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 Element of NAT ; :: thesis: ( n > 0 implies for i, j being Element of 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 ; :: thesis: for i, j being Element of 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 Element of NAT ; :: thesis: ( 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) ; :: thesis: 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:63;
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; :: thesis: verum