theorem Th25: :: SPRECT_5:25

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