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

per cases ( E-min (L~ z) = S-max (L~ z) or E-min (L~ z) <> S-max (L~ z) ) ;

suppose E-min (L~ z) = S-max (L~ z) ; :: thesis: (E-max (L~ z)) .. z < (S-max (L~ z)) .. z

hence (E-max (L~ z)) .. z < (S-max (L~ z)) .. z by A1, SPRECT_2:75; :: thesis: verum

end;

suppose E-min (L~ z) <> S-max (L~ z) ; :: thesis: (E-max (L~ z)) .. z < (S-max (L~ z)) .. z

thus (E-max (L~ z)) .. z < (S-max (L~ z)) .. z by A1, A2, SPRECT_2:76, XXREAL_0:2; :: thesis: verum

end;

end;