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 and
A2: k <= len (Cage C,n) and
A3: 1 <= t and
A4: t <= width (Gauge C,n) and
A5: (Cage C,n) /. k = (Gauge C,n) * 1,t ; :: thesis: (Cage C,n) /. k in W-most (L~ (Cage C,n))
len (Cage C,n) >= 2 by GOBOARD7:36, XXREAL_0:2;
then A6: (Cage C,n) /. k in L~ (Cage C,n) by A1, A2, TOPREAL3:46;
then A7: W-bound (L~ (Cage C,n)) <= ((Cage C,n) /. k) `1 by PSCOMP_1:71;
Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
then ((Gauge C,n) * 1,t) `1 <= W-bound (L~ (Cage C,n)) by A3, A4, Th42;
hence (Cage C,n) /. k in W-most (L~ (Cage C,n)) by A5, A6, A7, SPRECT_2:16, XXREAL_0:1; :: thesis: verum