theorem :: SPRECT_5:54

for z being constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-min (L~ z) & S-min (L~ z) <> W-min (L~ z) holds
(S-min (L~ z)) .. z < (W-min (L~ z)) .. z