:: deftheorem defines is_odd_substring_of GLIB_006:def 1 :
for D being non empty set
for f, g being FinSequence of D
for n being Nat holds
( g is_odd_substring_of f,n iff ( len g > 0 implies ex i being odd Nat st
( n <= i & i <= len f & mid (f,i,((i -' 1) + (len g))) = g ) ) );