let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, p, q being POINT of S st a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q holds
c,p equiv c,q
let a, b, c, p, q be POINT of S; :: thesis: ( a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q implies c,p equiv c,q )
assume A1: ( a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q ) ; :: thesis: c,p equiv c,q
a,b,c,p FS a,b,c,q

proof

( a,b equiv a,b & a,c equiv a,c & b,c equiv b,c ) by Satz2p1;
hence a,b,c,p FS a,b,c,q by A1, GTARSKI1:def 3; :: thesis: verum

end;

hence c,p equiv c,q by A1, Satz4p16; :: thesis: verum