let k, n, t be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) holds
(Cage (C,n)) /. k in E-most (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) implies (Cage (C,n)) /. k in E-most (L~ (Cage (C,n))) )
assume that
A1: ( 1 <= k & k <= len (Cage (C,n)) ) and
A2: ( 1 <= t & t <= width (Gauge (C,n)) ) and
A3: (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) ; :: thesis: (Cage (C,n)) /. k in E-most (L~ (Cage (C,n)))
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then A4: ((Gauge (C,n)) * ((len (Gauge (C,n))),t)) `1 >= E-bound (L~ (Cage (C,n))) by A2, Th23;
len (Cage (C,n)) >= 2 by GOBOARD7:34, XXREAL_0:2;
then A5: (Cage (C,n)) /. k in L~ (Cage (C,n)) by A1, TOPREAL3:39;
then E-bound (L~ (Cage (C,n))) >= ((Cage (C,n)) /. k) `1 by PSCOMP_1:24;
hence (Cage (C,n)) /. k in E-most (L~ (Cage (C,n))) by A3, A5, A4, SPRECT_2:13, XXREAL_0:1; :: thesis: verum