let z be constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = N-min (L~ z) implies (N-max (L~ z)) .. z < (S-max (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; :: thesis: (N-max (L~ z)) .. z < (S-max (L~ z)) .. z
then (N-max (L~ z)) .. z <= (E-max (L~ z)) .. z by SPRECT_2:70;
hence (N-max (L~ z)) .. z < (S-max (L~ z)) .. z by A1, Lm1, XXREAL_0:2; :: thesis: verum