let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: ex a, b, c being POINT of S st
( not between a,b,c & not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a )
consider a, b, c being POINT of S such that
A1: ( not between a,b,c & not between b,c,a & not between c,a,b ) by GTARSKI2:def 7;
take a ; :: thesis: ex b, c being POINT of S st
( not between a,b,c & not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a )
take b ; :: thesis: ex c being POINT of S st
( not between a,b,c & not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a )
take c ; :: thesis: ( not between a,b,c & not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a )
thus ( not between a,b,c & not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a ) by A1, Satz3p1; :: thesis: verum