let z be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( z /. 1 = N-min (L~ z) implies (S-max (L~ z)) .. z < (W-min (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; :: thesis: (S-max (L~ z)) .. z < (W-min (L~ z)) .. z
then A2: (S-max (L~ z)) .. z < (S-min (L~ z)) .. z by SPRECT_2:77;
per cases ( S-min (L~ z) = W-min (L~ z) or S-min (L~ z) <> W-min (L~ z) ) ;
suppose S-min (L~ z) = W-min (L~ z) ; :: thesis: (S-max (L~ z)) .. z < (W-min (L~ z)) .. z
hence (S-max (L~ z)) .. z < (W-min (L~ z)) .. z by A1, SPRECT_2:77; :: thesis: verum
end;
suppose S-min (L~ z) <> W-min (L~ z) ; :: thesis: (S-max (L~ z)) .. z < (W-min (L~ z)) .. z
thus (S-max (L~ z)) .. z < (W-min (L~ z)) .. z by A1, A2, SPRECT_2:78, XXREAL_0:2; :: thesis: verum
end;
end;