let z be constant standard clockwise_oriented special_circular_sequence; ( z /. 1 = W-min (L~ z) & W-max (L~ z) <> N-min (L~ z) implies (W-max (L~ z)) .. z < (N-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1:
L~ z = L~ (Rotate (z,(N-min (L~ z))))
by REVROT_1:33;
N-min (L~ z) in rng z
by SPRECT_2:39;
then A2:
(Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z)))))
by A1, FINSEQ_6:92;
then A3:
(W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) > (N-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z))))
by Lm8;
assume that
A4:
z /. 1 = W-min (L~ z)
and
A5:
W-max (L~ z) <> N-min (L~ z)
; (W-max (L~ z)) .. z < (N-min (L~ z)) .. z
for i being Nat st 1 < i & i < len z holds
z /. i <> z /. 1
by GOBOARD7:36;
then A6:
Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) = z
by A4, FINSEQ_6:181;
A7:
( N-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & W-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) )
by SPRECT_2:39, SPRECT_2:44;
( W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) )
by A1, A5, A2, SPRECT_2:43, SPRECT_2:75;
hence
(W-max (L~ z)) .. z < (N-min (L~ z)) .. z
by A1, A6, A7, A3, Th10; verum