:: deftheorem defines lies_between GOBOARD4:def 2 :
for f being FinSequence of REAL
for r, s being Real holds
( f lies_between r,s iff for n being Nat st n in dom f holds
( r <= f . n & f . n <= s ) );