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 <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,(width (Gauge (C,n)))) holds
(Cage (C,n)) /. k in N-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 <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,(width (Gauge (C,n)))) implies (Cage (C,n)) /. k in N-most (L~ (Cage (C,n))) )
assume that
A1: ( 1 <= k & k <= len (Cage (C,n)) ) and
A2: ( 1 <= t & t <= len (Gauge (C,n)) ) and
A3: (Cage (C,n)) /. k = (Gauge (C,n)) * (t,(width (Gauge (C,n)))) ; :: thesis: (Cage (C,n)) /. k in N-most (L~ (Cage (C,n)))
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then A4: ((Gauge (C,n)) * (t,(width (Gauge (C,n))))) `2 >= N-bound (L~ (Cage (C,n))) by A2, Th20;
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 N-bound (L~ (Cage (C,n))) >= ((Cage (C,n)) /. k) `2 by PSCOMP_1:24;
hence (Cage (C,n)) /. k in N-most (L~ (Cage (C,n))) by A3, A5, A4, SPRECT_2:10, XXREAL_0:1; :: thesis: verum