theorem Satz5p12: :: GTARSKI3:70

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S st Collinear a,b,c holds
( between a,b,c iff ( a,b <= a,c & b,c <= a,c ) )