:: deftheorem Def13 defines n_w_s JORDAN5D:def 13 :
for g being non constant standard special_circular_sequence
for b₂ being Nat holds
( b₂ = n_w_s g iff ( 1 <= b₂ & b₂ + 1 <= len g & g . b₂ = S-min (L~ g) ) );