let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: 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; :: thesis: 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; :: thesis: verum