for S being satisfying_Tarski-model TarskiGeometryStruct
for a, p being POINT of S st a <> p holds
p out a,a by Satz3p1;