let k, n, t be Nat; 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); ( 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)
; (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; verum