let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis:
let a, b, c be POINT of S; :: thesis:
assume A1: not Collinear a,b,c ; :: thesis:
then A2: a <> b by GTARSKI3:46;
consider x being POINT of S such that
A3: x is_foot a,b,c by A1, Satz8p18pExistence;
( Collinear a,b,x & are_orthogonal a,b,c,x ) by A3;
then are_orthogonal a,b,x,c,x by Satz8p15;
then A4: ( a <> b & c <> x & are_orthogonal Line (a,b),x, Line (c,x) ) ;
A5: ( a in Line (a,b) & c in Line (c,x) ) by GTARSKI3:83;
then right_angle a,x,c by A4;
then A6: a, reflection (x,c) equiv a,c by GTARSKI3:3;
Middle c,a, reflection (a,c) by GTARSKI3:def 13;
then a,c equiv a, reflection (a,c) by GTARSKI3:def 12;
then consider p being POINT of S such that
A7: Middle reflection (x,c),p, reflection (a,c) by A6, GTARSKI3:5, GTARSKI3:117;
A8: Middle reflection (a,c),p, reflection (x,c) by A7, GTARSKI3:96;
A9: right_angle a,x,c by A5, A4;
then A10: ( right_angle x,a,p & a <> p ) by A1, A3, A8, Lemma8p20;

now :: thesis:

Middle c,x, reflection (x,c) by GTARSKI3:def 13;
hence between reflection (x,c),x,c by GTARSKI3:14, GTARSKI3:def 12; :: thesis:
Middle c,a, reflection (a,c) by GTARSKI3:def 13;
hence between reflection (a,c),a,c by GTARSKI3:14, GTARSKI3:def 12; :: thesis:
thus between reflection (x,c),p, reflection (a,c) by A7, GTARSKI3:def 12; :: thesis:

end;

then consider t being POINT of S such that
A11: between p,t,c and
A12: between x,t,a by GTARSKI3:40;
Collinear x,t,a by A12, GTARSKI1:def 17;
then Collinear x,a,t by GTARSKI3:45;
then A13: t in Line (x,a) by LemmaA1;

per cases ;

suppose A16: x <> a ; :: thesis:

then Line (a,b) = Line (x,a) by A2, A3, LemmaA1, GTARSKI3:82;
then a18: Collinear t,a,b by LemmaA2, A13;
take p ; :: thesis:
take t ; :: thesis:

now :: thesis:

thus a <> b by A1, GTARSKI3:46; :: thesis:
thus p <> a by A9, A1, A3, A8, Lemma8p20; :: thesis:

now :: thesis:

thus Line (a,b) is_line by A2, GTARSKI3:def 11; :: thesis:
thus Line (p,a) is_line by A10, GTARSKI3:def 11; :: thesis:
thus a in Line (a,b) by GTARSKI3:83; :: thesis:
thus a in Line (p,a) by GTARSKI3:83; :: thesis:
thus ex u, v being POINT of S st
( u in Line (a,b) & v in Line (p,a) & u <> a & v <> a & right_angle u,a,v ) :: thesis:

proof

take x ; :: thesis:
take p ; :: thesis:
thus x in Line (a,b) by A3, LemmaA1; :: thesis:
thus p in Line (p,a) by GTARSKI3:83; :: thesis:
thus ( x <> a & p <> a ) by A16, A9, A1, A3, A8, Lemma8p20; :: thesis:
thus right_angle x,a,p by A9, A8, Lemma8p20; :: thesis:

end;

end;

hence are_orthogonal Line (a,b), Line (p,a) by Satz8p13; :: thesis:

end;

hence ( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p ) by a18, A11, GTARSKI3:14, GTARSKI3:45; :: thesis:

end;

suppose A19: x = a ; :: thesis:

then A20: a = t by A12, GTARSKI1:def 10;

a21: now :: thesis:

thus p <> a by A9, A1, A3, A8, Lemma8p20; :: thesis:
thus c <> a :: thesis:

proof

assume c = a ; :: thesis:
then Collinear a,c,b by GTARSKI3:46;
hence contradiction by A1, GTARSKI3:45; :: thesis:

end;

Collinear p,a,c by A20, A11, GTARSKI1:def 17;
hence c in Line (a,p) by LemmaA1; :: thesis:

end;

take p ; :: thesis:
take t ; :: thesis:
( Collinear a,b,a & are_orthogonal a,b,c,a ) by A3, A19;
hence ( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p ) by a21, A11, GTARSKI3:14, GTARSKI3:82, A19, A12, GTARSKI1:def 10; :: thesis:

end;

end;