let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, d being POINT of S st a <> b & Collinear a,b,c & Collinear a,b,d holds
Collinear a,c,d
let a, b, c, d be POINT of S; ( a <> b & Collinear a,b,c & Collinear a,b,d implies Collinear a,c,d )
assume that
A1:
a <> b
and
A2:
Collinear a,b,c
and
A3:
Collinear a,b,d
; Collinear a,c,d
per cases
( a = c or a <> c )
;
suppose
a <> c
;
Collinear a,c,dthen A4:
Line (
a,
b)
= Line (
a,
c)
by A1, A2, Prelim07;
d in { y where y is POINT of S : Collinear a,b,y }
by A3;
then
d in Line (
a,
c)
by A4, GTARSKI3:def 10;
then
Collinear d,
a,
c
by LemmaA2;
hence
Collinear a,
c,
d
by GTARSKI3:45;
verum end; end;