:: deftheorem Def3 defines i_s_e JORDAN5D:def 3 :
for g being non constant standard special_circular_sequence
for b₂ being Nat holds
( b₂ = i_s_e g iff ( [(len (GoB g)),b₂] in Indices (GoB g) & (GoB g) * ((len (GoB g)),b₂) = E-min (L~ g) ) );