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