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,1)),((Gauge (C,n)) * (i,j))) meets Lower_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,1)),((Gauge (C,n)) * (i,j))) meets Lower_Arc (L~ (Cage (C,n))) )
assume 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,1)),((Gauge (C,n)) * (i,j))) meets Lower_Arc (L~ (Cage (C,n)))
then A1: L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) by Th56;
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,1)),((Gauge (C,n)) * (i,j))) meets Lower_Arc (L~ (Cage (C,n))) )
assume ( 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) ) ; :: thesis: LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets Lower_Arc (L~ (Cage (C,n)))
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,j))) meets Lower_Arc (L~ (Cage (C,n))) by A1, Th46; :: thesis: verum