let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i <= len (Gauge C,n) holds
LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Upper_Arc (L~ (Cage C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i being Element of NAT st 1 <= i & i <= len (Gauge C,n) holds
LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Upper_Arc (L~ (Cage C,n))
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len (Gauge C,n) implies LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Upper_Arc (L~ (Cage C,n)) )
assume A1: ( 1 <= i & i <= len (Gauge C,n) ) ; :: thesis: LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Upper_Arc (L~ (Cage C,n))
A2: (Gauge C,n) * i,1 = |[(((Gauge C,n) * i,1) `1 ),(((Gauge C,n) * i,1) `2 )]| by EUCLID:57
.= |[(((Gauge C,n) * i,1) `1 ),(S-bound (L~ (Cage C,n)))]| by A1, JORDAN1A:93 ;
A3: (Gauge C,n) * i,(len (Gauge C,n)) = |[(((Gauge C,n) * i,(len (Gauge C,n))) `1 ),(((Gauge C,n) * i,(len (Gauge C,n))) `2 )]| by EUCLID:57
.= |[(((Gauge C,n) * i,(len (Gauge C,n))) `1 ),(N-bound (L~ (Cage C,n)))]| by A1, JORDAN1A:91 ;
set r = ((Gauge C,n) * i,1) `1 ;
A4: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
4 <= len (Gauge C,n) by JORDAN8:13;
then A5: 1 <= len (Gauge C,n) by XXREAL_0:2;
then A6: ((Gauge C,n) * i,1) `1 = ((Gauge C,n) * i,(len (Gauge C,n))) `1 by A1, A4, GOBOARD5:3;
((Gauge C,n) * 1,1) `1 <= ((Gauge C,n) * i,1) `1 by A1, A4, A5, SPRECT_3:25;
then A7: W-bound (L~ (Cage C,n)) <= ((Gauge C,n) * i,1) `1 by A5, JORDAN1A:94;
((Gauge C,n) * i,1) `1 <= ((Gauge C,n) * (len (Gauge C,n)),1) `1 by A1, A4, A5, SPRECT_3:25;
then ((Gauge C,n) * i,1) `1 <= E-bound (L~ (Cage C,n)) by A5, JORDAN1A:92;
hence LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,(len (Gauge C,n))) meets Upper_Arc (L~ (Cage C,n)) by A2, A3, A6, A7, JORDAN6:84; :: thesis: verum