let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for x, y, a, b, c being POINT of S st x is_foot a,b,c & y is_foot a,b,c holds
x = y
let x, y, a, b, c be POINT of S; :: thesis: ( x is_foot a,b,c & y is_foot a,b,c implies x = y )
assume that
A1: x is_foot a,b,c and
A2: y is_foot a,b,c ; :: thesis: x = y
A3: ( Collinear a,b,y & are_orthogonal a,b,c,y ) by A2;
A4: ( c in Line (c,x) & c in Line (c,y) ) by GTARSKI3:83;
( are_orthogonal a,b,x,c,x & are_orthogonal a,b,y,c,y ) by A1, A3, Satz8p15;
then ( are_orthogonal Line (a,b),x, Line (c,x) & are_orthogonal Line (a,b),y, Line (c,y) ) ;
then ( right_angle c,x,y & right_angle c,y,x ) by A4, Satz8p2;
hence x = y by Satz8p7; :: thesis: verum