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

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