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