let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, x, p being POINT of S st x in Line (a,p) holds
Collinear x,a,p
let a, x, p be POINT of S; :: thesis: ( x in Line (a,p) implies Collinear x,a,p )
assume x in Line (a,p) ; :: thesis: Collinear x,a,p
then x in { y where y is POINT of S : Collinear a,p,y } by GTARSKI3:def 10;
then ex y being POINT of S st
( x = y & Collinear a,p,y ) ;
hence Collinear x,a,p by GTARSKI3:45; :: thesis: verum