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,1),((Gauge C,n) * i,j) meets Lower_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,1),((Gauge C,n) * i,j) meets Lower_Arc (L~ (Cage C,n)) )
assume 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,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 Th64;
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,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, Th54; :: thesis: verum