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