let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; for a, b being POINT of S ex c being POINT of S st
( between a,b,c & b <> c )
let a, b be POINT of S; ex c being POINT of S st
( between a,b,c & b <> c )
consider u, v, w being POINT of S such that
A1:
( not between u,v,w & not between v,w,u & not between w,u,v & u <> v & v <> w & w <> u )
by Satz3p13;
consider x being POINT of S such that
A2:
( between a,b,x & b,x equiv u,v )
by GTARSKI1:def 8;
b <> x
by A1, A2, Satz2p2, GTARSKI1:def 7;
hence
ex c being POINT of S st
( between a,b,c & b <> c )
by A2; verum