:: deftheorem Def5 defines i_w_s JORDAN5D:def 5 :
for g being non constant standard special_circular_sequence
for b2 being Nat holds
( b2 = i_w_s g iff ( [b2,1] in Indices (GoB g) & (GoB g) * (b2,1) = S-min (L~ g) ) );