let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; for p, q, r being POINT of S st p <> q & p <> r & ( Collinear p,q,r or Collinear q,r,p or Collinear r,p,q or Collinear p,r,q or Collinear q,p,r or Collinear r,q,p ) holds
( Line (p,q) = Line (p,r) & Line (p,q) = Line (r,p) & Line (q,p) = Line (p,r) & Line (q,p) = Line (r,p) )
let p, q, r be POINT of S; ( p <> q & p <> r & ( Collinear p,q,r or Collinear q,r,p or Collinear r,p,q or Collinear p,r,q or Collinear q,p,r or Collinear r,q,p ) implies ( Line (p,q) = Line (p,r) & Line (p,q) = Line (r,p) & Line (q,p) = Line (p,r) & Line (q,p) = Line (r,p) ) )
assume that
A1:
p <> q
and
A2:
p <> r
and
A3:
( Collinear p,q,r or Collinear q,r,p or Collinear r,p,q or Collinear p,r,q or Collinear q,p,r or Collinear r,q,p )
; ( Line (p,q) = Line (p,r) & Line (p,q) = Line (r,p) & Line (q,p) = Line (p,r) & Line (q,p) = Line (r,p) )
Collinear p,q,r
by A3, GTARSKI3:45;
then
r on_line p,q
by A1, GTARSKI3:84;
hence
( Line (p,q) = Line (p,r) & Line (p,q) = Line (r,p) & Line (q,p) = Line (p,r) & Line (q,p) = Line (r,p) )
by A1, A2, GTARSKI1:39, GTARSKI3:85; verum