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