theorem :: GTARSKI3:116

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for c, a1, a2, b1, b2, m1, m2 being POINT of S st Krippenfigur a1,m1,b1,c,b2,m2,a2 holds
between m1,c,m2 by Satz7p22;