theorem :: SPRECT_3:31

for f being constant standard clockwise_oriented special_circular_sequence st f /. 1 = N-min (L~ f) holds
LSeg ((f /. 1),(f /. 2)) c= L~ (SpStSeq (L~ f))