theorem Th72: :: SPRECT_2:72

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