let z be non constant standard clockwise_oriented special_circular_sequence; ( z /. 1 = S-max (L~ z) & E-min (L~ z) <> S-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;
assume A2:
z /. 1 = S-max (L~ z)
; ( not E-min (L~ z) <> S-max (L~ z) or (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 A3:
Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) = z
by A2, REVROT_1:16;
A4:
( E-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & E-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) )
by SPRECT_2:49, SPRECT_2:50;
W-min (L~ z) in rng z
by SPRECT_2:47;
then A5:
(Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z)))))
by A1, FINSEQ_6:98;
then A6:
( S-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (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 Th27, SPRECT_2:46;
assume
E-min (L~ z) <> S-max (L~ z)
; (E-max (L~ z)) .. z < (E-min (L~ z)) .. z
then
(E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z))))
by A1, A5, Th28;
hence
(E-max (L~ z)) .. z < (E-min (L~ z)) .. z
by A1, A3, A4, A6, Th12; verum