let z be constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = E-max (L~ z) implies (W-min (L~ z)) .. z < (W-max (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
S-max (L~ z) in rng z by SPRECT_2:42;
then (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (W-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) & (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by Lm21, Th32;
A3: E-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) by SPRECT_2:46;
assume A4: z /. 1 = E-max (L~ z) ; :: thesis: (W-min (L~ z)) .. z < (W-max (L~ z)) .. z
for i being Nat st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(S-max (L~ z)))),(E-max (L~ z))) = z by A4, FINSEQ_6:181;
( W-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & W-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:43, SPRECT_2:44;
hence (W-min (L~ z)) .. z < (W-max (L~ z)) .. z by A1, A5, A3, A2, Th11; :: thesis: verum