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) * (len (Gauge C,n)),t holds
(Cage C,n) /. k in E-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) * (len (Gauge C,n)),t implies (Cage C,n) /. k in E-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) * (len (Gauge C,n)),t ; :: thesis: (Cage C,n) /. k in E-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: E-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) * (len (Gauge C,n)),t) `1 >= E-bound (L~ (Cage C,n)) by A3, A4, Th44;
hence (Cage C,n) /. k in E-most (L~ (Cage C,n)) by A5, A6, A7, SPRECT_2:17, XXREAL_0:1; :: thesis: verum