theorem :: JORDAN5B:16

for g1 being FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i <= len g1 & g1 is being_S-Seq & g1 /. 1 in L~ (mid (g1,i,(len g1))) holds
i = 1