let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being 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 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 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 that
A1: 1 <= i and
A2: 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)))
A3: (Gauge (C,n)) * (i,1) = |[(((Gauge (C,n)) * (i,1)) `1),(((Gauge (C,n)) * (i,1)) `2)]| by EUCLID:53
.= |[(((Gauge (C,n)) * (i,1)) `1),(S-bound (L~ (Cage (C,n))))]| by A1, A2, JORDAN1A:72 ;
A4: (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:53
.= |[(((Gauge (C,n)) * (i,(len (Gauge (C,n))))) `1),(N-bound (L~ (Cage (C,n))))]| by A1, A2, JORDAN1A:70 ;
set r = ((Gauge (C,n)) * (i,1)) `1 ;
4 <= len (Gauge (C,n)) by JORDAN8:10;
then A5: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
A6: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then ((Gauge (C,n)) * (1,1)) `1 <= ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A5, SPRECT_3:13;
then A7: W-bound (L~ (Cage (C,n))) <= ((Gauge (C,n)) * (i,1)) `1 by A5, JORDAN1A:73;
((Gauge (C,n)) * (i,1)) `1 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 by A1, A2, A6, A5, SPRECT_3:13;
then A8: ((Gauge (C,n)) * (i,1)) `1 <= E-bound (L~ (Cage (C,n))) by A5, JORDAN1A:71;
((Gauge (C,n)) * (i,1)) `1 = ((Gauge (C,n)) * (i,(len (Gauge (C,n))))) `1 by A1, A2, A6, A5, GOBOARD5:2;
hence LSeg (((Gauge (C,n)) * (i,1)),((Gauge (C,n)) * (i,(len (Gauge (C,n)))))) meets Upper_Arc (L~ (Cage (C,n))) by A3, A4, A7, A8, JORDAN6:69; :: thesis: verum