let z be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = E-min (L~ z) & E-max (L~ z) <> N-max (L~ z) implies (N-max (L~ z)) .. z < (E-max (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
W-min (L~ z) in rng z by SPRECT_2:47;
then A2: (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:98;
then A3: (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) by Th27;
assume that
A4: z /. 1 = E-min (L~ z) and
A5: E-max (L~ z) <> N-max (L~ z) ; :: thesis: (N-max (L~ z)) .. z < (E-max (L~ z)) .. z
for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:38;
then A6: Rotate ((Rotate (z,(W-min (L~ z)))),(E-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( E-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & N-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:44, SPRECT_2:50;
( E-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & (N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by A1, A5, A2, Th26, SPRECT_2:49;
hence (N-max (L~ z)) .. z < (E-max (L~ z)) .. z by A1, A6, A7, A3, Th12; :: thesis: verum