let k, n, t be Element of 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, Th43;
len (Cage C,n) >= 2 by GOBOARD7:36, XXREAL_0:2;
then A5: (Cage C,n) /. k in L~ (Cage C,n) by A1, TOPREAL3:46;
then S-bound (L~ (Cage C,n)) <= ((Cage C,n) /. k) `2 by PSCOMP_1:71;
hence (Cage C,n) /. k in S-most (L~ (Cage C,n)) by A3, A5, A4, SPRECT_2:15, XXREAL_0:1; :: thesis: verum