:: deftheorem defines between GTARSKI5:def 1 :
for S being non empty TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S holds
( between a,A,b iff ( A is_line & not a in A & not b in A & ex t being POINT of S st
( t in A & between a,t,b ) ) );