:: deftheorem defines between GTARSKI1:def 1 :
for S being TarskiGeometryStruct
for a, b, c being POINT of S holds
( between a,b,c iff [[a,b],c] in the Betweenness of S );