let z be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = S-max (L~ z) implies (N-min (L~ z)) .. z < (N-max (L~ z)) .. z )
set g = Rotate z,(W-min (L~ z));
A1: for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:38;
A2: W-min (L~ z) in rng z by SPRECT_2:47;
A3: L~ z = L~ (Rotate z,(W-min (L~ z))) by REVROT_1:33;
assume A4: z /. 1 = S-max (L~ z) ; :: thesis: (N-min (L~ z)) .. z < (N-max (L~ z)) .. z
A5: Rotate (Rotate z,(W-min (L~ z))),(S-max (L~ z)) = z by A1, A4, REVROT_1:16;
A6: (Rotate z,(W-min (L~ z))) /. 1 = W-min (L~ (Rotate z,(W-min (L~ z)))) by A2, A3, FINSEQ_6:98;
A7: N-max (L~ (Rotate z,(W-min (L~ z)))) in rng (Rotate z,(W-min (L~ z))) by SPRECT_2:44;
A8: N-min (L~ (Rotate z,(W-min (L~ z)))) in rng (Rotate z,(W-min (L~ z))) by SPRECT_2:43;
A9: S-max (L~ (Rotate z,(W-min (L~ z)))) in rng (Rotate z,(W-min (L~ z))) by SPRECT_2:46;
A10: (N-min (L~ (Rotate z,(W-min (L~ z))))) .. (Rotate z,(W-min (L~ z))) < (N-max (L~ (Rotate z,(W-min (L~ z))))) .. (Rotate z,(W-min (L~ z))) by A6, Th25;
(N-max (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 A6, Lm14;
hence (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by A3, A5, A7, A8, A9, A10, Th12; :: thesis: verum