:: deftheorem defines Collinear GTARSKI1:def 17 :
for S being TarskiGeometryStruct
for a, b, c being POINT of S holds
( Collinear a,b,c iff ( between a,b,c or between b,c,a or between c,a,b ) );