let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( 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 )
; 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;
verum
end;
hence
c,p equiv c,q
by A1, Satz4p16; verum