theorem Satz3p15p4: :: GTARSKI3:38

for S being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a1, a2 being POINT of S st a1 <> a2 holds
ex a3, a4 being POINT of S st
( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct )