:: deftheorem defines is_foot GTARSKI4:def 8 :
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, x being POINT of S holds
( x is_foot a,b,c iff ( Collinear a,b,x & are_orthogonal a,b,c,x ) );