:: deftheorem defines lies_between GOBOARD4:def 1 :
for f being Relation
for r, s being Real holds
( f lies_between r,s iff rng f c= [.r,s.] );