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,1) holds
(Cage (C,n)) /. k in S-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,1) implies (Cage (C,n)) /. k in S-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,1) ; :: thesis: (Cage (C,n)) /. k in S-most (L~ (Cage (C,n)))
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then A4: ((Gauge (C,n)) * (t,1)) `2 <= S-bound (L~ (Cage (C,n))) by A2, Th22;
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 S-bound (L~ (Cage (C,n))) <= ((Cage (C,n)) /. k) `2 by PSCOMP_1:24;
hence (Cage (C,n)) /. k in S-most (L~ (Cage (C,n))) by A3, A5, A4, SPRECT_2:11, XXREAL_0:1; :: thesis: verum