let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: 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: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; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: 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; :: 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: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; :: thesis: verum