let f be non constant standard special_circular_sequence; :: thesis: i_w_n f < i_e_n f
set G = GoB f;
A1: width (GoB f) > 1 by GOBOARD7:35;
A2: i_w_n f <= len (GoB f) by JORDAN5D:47;
A3: (GoB f) * (i_w_n f),(width (GoB f)) = N-min (L~ f) by JORDAN5D:def 7;
A4: 1 <= i_e_n f by JORDAN5D:47;
A5: (GoB f) * (i_e_n f),(width (GoB f)) = N-max (L~ f) by JORDAN5D:def 8;
A6: (N-min (L~ f)) `1 < (N-max (L~ f)) `1 by SPRECT_2:55;
then A7: i_w_n f <> i_e_n f by A5, JORDAN5D:def 7;
assume i_w_n f >= i_e_n f ; :: thesis: contradiction
then i_w_n f > i_e_n f by A7, XXREAL_0:1;
hence contradiction by A1, A2, A3, A4, A5, A6, GOBOARD5:4; :: thesis: verum