let S be 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 )
let a1, a2 be POINT of S; ( a1 <> a2 implies ex a3 being POINT of S st
( between a1,a2,a3 & a1,a2,a3 are_mutually_distinct ) )
assume A1:
a1 <> a2
; ex a3 being POINT of S st
( between a1,a2,a3 & a1,a2,a3 are_mutually_distinct )
consider a3 being POINT of S such that
A2:
( between a1,a2,a3 & a2 <> a3 )
by Satz3p14;
a1 <> a3
by A2, GTARSKI1:def 10;
hence
ex a3 being POINT of S st
( between a1,a2,a3 & a1,a2,a3 are_mutually_distinct )
by A1, A2, ZFMISC_1:def 5; verum