theorem Thequiv1: :: GTARSKI3:84

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being Element of S holds
( ( a <> b & Collinear a,b,c ) iff c on_line a,b ) ;