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