let z be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = S-max (L~ z) implies (W-max (L~ z)) .. z < (N-max (L~ z)) .. z )
assume A1: z /. 1 = S-max (L~ z) ; :: thesis: (W-max (L~ z)) .. z < (N-max (L~ z)) .. z
then A2: (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by Th35;

per cases ( W-max (L~ z) = N-min (L~ z) or W-max (L~ z) <> N-min (L~ z) ) ;

suppose W-max (L~ z) = N-min (L~ z) ; :: thesis: (W-max (L~ z)) .. z < (N-max (L~ z)) .. z

hence (W-max (L~ z)) .. z < (N-max (L~ z)) .. z by A1, Th35; :: thesis: verum

end;

suppose W-max (L~ z) <> N-min (L~ z) ; :: thesis: (W-max (L~ z)) .. z < (N-max (L~ z)) .. z

thus (W-max (L~ z)) .. z < (N-max (L~ z)) .. z by A1, A2, Th34, XXREAL_0:2; :: thesis: verum

end;

end;