theorem Satz8p18pExistence: :: GTARSKI4:33

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st not Collinear a,b,c holds
ex x being POINT of S st x is_foot a,b,c