let z be non constant standard clockwise_oriented special_circular_sequence; ( z /. 1 = E-max (L~ z) & S-max (L~ z) <> E-min (L~ z) implies (E-min (L~ z)) .. z < (S-max (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:43;
then A2:
(Rotate z,(N-min (L~ z))) /. 1 = N-min (L~ (Rotate z,(N-min (L~ z))))
by A1, FINSEQ_6:98;
then A3:
( E-min (L~ (Rotate z,(N-min (L~ z)))) in rng (Rotate z,(N-min (L~ z))) & (E-max (L~ (Rotate z,(N-min (L~ z))))) .. (Rotate z,(N-min (L~ z))) < (E-min (L~ (Rotate z,(N-min (L~ z))))) .. (Rotate z,(N-min (L~ z))) )
by SPRECT_2:49, SPRECT_2:75;
assume that
A4:
z /. 1 = E-max (L~ z)
and
A5:
S-max (L~ z) <> E-min (L~ z)
; (E-min (L~ z)) .. z < (S-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,(N-min (L~ z))),(E-max (L~ z)) = z
by A4, REVROT_1:16;
A7:
( S-max (L~ (Rotate z,(N-min (L~ z)))) in rng (Rotate z,(N-min (L~ z))) & E-max (L~ (Rotate z,(N-min (L~ z)))) in rng (Rotate z,(N-min (L~ z))) )
by SPRECT_2:46, SPRECT_2:50;
(E-min (L~ (Rotate z,(N-min (L~ z))))) .. (Rotate z,(N-min (L~ z))) < (S-max (L~ (Rotate z,(N-min (L~ z))))) .. (Rotate z,(N-min (L~ z)))
by A1, A5, A2, SPRECT_2:76;
hence
(E-min (L~ z)) .. z < (S-max (L~ z)) .. z
by A1, A6, A7, A3, Th5; verum