let f be non constant standard special_circular_sequence; :: thesis: ( f /. 1 = N-min (L~ f) implies ( f is clockwise_oriented iff f /. 2 in N-most (L~ f) ) )
assume f /. 1 = N-min (L~ f) ; :: thesis: ( f is clockwise_oriented iff f /. 2 in N-most (L~ f) )
then Rotate (f,(N-min (L~ f))) = f by FINSEQ_6:95;
hence ( f is clockwise_oriented iff f /. 2 in N-most (L~ f) ) by Def4; :: thesis: verum