let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( a1 <> a2 implies ex a3 being POINT of S st
( between a1,a2,a3 & a1,a2,a3 are_mutually_distinct ) )
assume A1: a1 <> a2 ; :: thesis: 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; :: thesis: verum