theorem Satz3p15p3: :: GTARSKI3:37

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a1, a2 being POINT of S st a1 <> a2 holds
ex a3 being POINT of S st
( between a1,a2,a3 & a1,a2,a3 are_mutually_distinct )