let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st a <> b holds
ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )
let a, b, c be POINT of S; :: thesis: ( a <> b implies ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p ) )
assume A1: a <> b ; :: thesis: ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )

per cases ( not Collinear a,b,c or Collinear a,b,c ) ;

suppose not Collinear a,b,c ; :: thesis: ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )

hence ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p ) by Satz8p21p1; :: thesis: verum

end;

suppose A2: Collinear a,b,c ; :: thesis: ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )

consider c9 being POINT of S such that
A3: not Collinear a,b,c9 by A1, GTARSKI3:92;
ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c9,t,p ) by A3, Satz8p21p1;
hence ex p, t being POINT of S st
( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p ) by A2, GTARSKI3:15; :: thesis: verum

end;

end;