:: deftheorem defines equal_line GTARSKI1:def 19 :
for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, x, y being POINT of S holds
( a,b equal_line x,y iff ( a <> b & x <> y & ( for c being POINT of S holds
( c on_line a,b iff c on_line x,y ) ) ) );