let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, c9 being POINT of S st a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9 holds
c = c9
let a, b, c, c9 be POINT of S; :: thesis: ( a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9 implies c = c9 )
assume ( a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9 ) ; :: thesis: c = c9
then c,c equiv c,c9 by Satz4p17;
hence c = c9 by Satz2p2, GTARSKI1:def 7; :: thesis: verum