let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; ex p, q being POINT of S st p <> q
assume A1:
for p, q being POINT of S holds not p <> q
; contradiction
consider a, b, c being POINT of S such that
A2:
not between a,b,c
and
not between b,c,a
and
not between c,a,b
by GTARSKI2:def 7;
( a = b & a = c )
by A1;
hence
contradiction
by A2, GTARSKI3:15; verum