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