let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: 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
let a, b, c be POINT of S; :: thesis: ( not Collinear a,b,c implies ex x being POINT of S st x is_foot a,b,c )
assume A1: not Collinear a,b,c ; :: thesis: ex x being POINT of S st x is_foot a,b,c
consider y being POINT of S such that
A2: between b,a,y and
A3: a,y equiv a,c by GTARSKI1:def 8;
consider p being POINT of S such that
A4: Middle y,p,c by A3, GTARSKI3:117;
A5: right_angle a,p,y by A3, A4, GTARSKI3:def 13;
consider z being POINT of S such that
A6: between a,y,z and
A7: y,z equiv y,p by GTARSKI1:def 8;
consider q being POINT of S such that
A8: between p,y,q and
A9: y,q equiv y,a by GTARSKI1:def 8;
set q9 = reflection (z,q);
consider c9 being POINT of S such that
A10: between reflection (z,q),y,c9 and
A11: y,c9 equiv y,c by GTARSKI1:def 8;
A12: a <> b by A1, GTARSKI3:46;
A13: a <> y

proof

assume a = y ; :: thesis: contradiction
then a = c by A3, GTARSKI1:def 7, GTARSKI3:4;
then Collinear a,c,b by GTARSKI3:46;
hence contradiction by A1, GTARSKI3:45; :: thesis: verum

end;

now :: thesis: ( between a,y,z & between q,y,p & a,y equiv q,y & y,z equiv y,p & a,q equiv q,a & y,q equiv y,a )

thus between a,y,z by A6; :: thesis: ( between q,y,p & a,y equiv q,y & y,z equiv y,p & a,q equiv q,a & y,q equiv y,a )
thus between q,y,p by A8, GTARSKI3:14; :: thesis: ( a,y equiv q,y & y,z equiv y,p & a,q equiv q,a & y,q equiv y,a )
y,a equiv y,q by A9, GTARSKI3:3;
then a,y equiv y,q by GTARSKI3:6;
hence a,y equiv q,y by GTARSKI3:7; :: thesis: ( y,z equiv y,p & a,q equiv q,a & y,q equiv y,a )
thus y,z equiv y,p by A7; :: thesis: ( a,q equiv q,a & y,q equiv y,a )
thus a,q equiv q,a by GTARSKI3:2, GTARSKI3:6; :: thesis: y,q equiv y,a
thus y,q equiv y,a by A9; :: thesis: verum

end;

then A14: a,y,z,q AFS q,y,p,a by GTARSKI3:def 2;

now :: thesis: ( a,p equiv q,z & a,y equiv q,y & p,y equiv z,y )

p,a equiv z,q by A14, A13, GTARSKI3:3, GTARSKI3:10;
then a,p equiv z,q by GTARSKI3:6;
hence a,p equiv q,z by GTARSKI3:7; :: thesis: ( a,y equiv q,y & p,y equiv z,y )
y,a equiv y,q by A9, GTARSKI3:3;
then a,y equiv y,q by GTARSKI3:6;
hence a,y equiv q,y by GTARSKI3:7; :: thesis: p,y equiv z,y
y,p equiv y,z by A7, GTARSKI3:4;
then p,y equiv y,z by GTARSKI3:6;
hence p,y equiv z,y by GTARSKI3:7; :: thesis: verum

end;

then a,p,y cong q,z,y by GTARSKI1:def 3;
then right_angle q,z,y by A5, Satz8p10;
then A15: right_angle y,z,q by Satz8p2;
A16: y,c equiv y,c9 by A11, GTARSKI3:3;
consider x being POINT of S such that
A17: Middle c,x,c9 by A11, GTARSKI3:3, GTARSKI3:117;
A18: y <> p

proof

assume y = p ; :: thesis: contradiction
then y,c equiv y,y by A4, GTARSKI3:4, GTARSKI3:def 12;
then y = c by GTARSKI1:def 7;
then Collinear b,a,c by A2, GTARSKI1:def 17;
hence contradiction by A1, GTARSKI3:45; :: thesis: verum

end;

now :: thesis: ( between q,y,c & between reflection (z,q),y,c9 & y,q equiv y, reflection (z,q) & y,c equiv y,c9 & Middle q,z, reflection (z,q) & Middle c,x,c9 )

( between q,y,p & between y,p,c ) by A4, A8, GTARSKI3:14, GTARSKI3:def 12;
hence between q,y,c by A18, GTARSKI3:19; :: thesis: ( between reflection (z,q),y,c9 & y,q equiv y, reflection (z,q) & y,c equiv y,c9 & Middle q,z, reflection (z,q) & Middle c,x,c9 )
thus between reflection (z,q),y,c9 by A10; :: thesis: ( y,q equiv y, reflection (z,q) & y,c equiv y,c9 & Middle q,z, reflection (z,q) & Middle c,x,c9 )
thus y,q equiv y, reflection (z,q) by A15; :: thesis: ( y,c equiv y,c9 & Middle q,z, reflection (z,q) & Middle c,x,c9 )
thus y,c equiv y,c9 by A11, GTARSKI3:3; :: thesis: ( Middle q,z, reflection (z,q) & Middle c,x,c9 )
thus Middle q,z, reflection (z,q) by GTARSKI3:def 13; :: thesis: Middle c,x,c9
thus Middle c,x,c9 by A17; :: thesis: verum

end;

then Krippenfigur q,z, reflection (z,q),y,c9,x,c by GTARSKI3:def 14;
then between z,y,x by GTARSKI3:116;
then A19: Collinear z,y,x by GTARSKI1:def 17;
A20: c <> y

proof

assume y = c ; :: thesis: contradiction
then Collinear b,a,c by A2, GTARSKI1:def 17;
hence contradiction by A1, GTARSKI3:45; :: thesis: verum

end;

A21: y <> z by A7, A18, GTARSKI1:def 7, GTARSKI3:4;
A22: q <> reflection (z,q)

proof

assume q = reflection (z,q) ; :: thesis: contradiction
then A23: Middle q,z,q by GTARSKI3:def 13;
then A24: q = z by GTARSKI3:97;
A25: y <> q by A23, GTARSKI3:97, A21;
Collinear b,a,y by A2, GTARSKI1:def 17;
then A26: Line (y,a) = Line (a,b) by A12, A13, GTARSKI3:82, LemmaA1;
Collinear a,y,z by A6, GTARSKI1:def 17;
then A27: Line (y,q) = Line (a,b) by A13, A21, A26, GTARSKI3:82, A24, LemmaA1;
Collinear y,q,p by A8, GTARSKI1:def 17;
then A28: Line (y,p) = Line (a,b) by A25, A18, GTARSKI3:82, A27, LemmaA1;
between y,p,c by A4, GTARSKI3:def 12;
then Collinear y,p,c by GTARSKI1:def 17;
then c in Line (a,b) by A28, LemmaA1;
then Collinear c,a,b by LemmaA2;
hence contradiction by A1, GTARSKI3:45; :: thesis: verum

end;

now :: thesis: ( y in Line (a,b) & a <> y & a <> b )

Collinear b,a,y by A2, GTARSKI1:def 17;
hence y in Line (a,b) by LemmaA1; :: thesis: ( a <> y & a <> b )
thus a <> y by A13; :: thesis: a <> b
thus a <> b by A1, GTARSKI3:46; :: thesis: verum

end;

then A29: Line (a,y) = Line (a,b) by GTARSKI3:82;

now :: thesis: ( z in Line (y,a) & y <> a & y <> z )

Collinear a,y,z by A6, GTARSKI1:def 17;
hence z in Line (y,a) by LemmaA1; :: thesis: ( y <> a & y <> z )
thus y <> a by A13; :: thesis: y <> z
thus y <> z by A7, A18, GTARSKI1:def 7, GTARSKI3:4; :: thesis: verum

end;

then A30: Line (y,z) = Line (a,b) by A29, GTARSKI3:82;
A31: c <> x

proof

assume c = x ; :: thesis: contradiction
then c9 = reflection (c,c) by A17, GTARSKI3:def 13;
then between reflection (z,q),y,c by A10, GTARSKI3:104;
then a32: Collinear y,c, reflection (z,q) by GTARSKI1:def 17;
between y,p,c by A4, GTARSKI3:def 12;
then A33: Collinear y,p,c by GTARSKI1:def 17;
A34: q <> y by A13, A9, GTARSKI3:4, GTARSKI1:def 7;
y <> p by A4, A20, Prelim09;
then A35: Line (y,p) = Line (y,c) by A20, A33, GTARSKI3:82, LemmaA1;
Collinear p,y,q by A8, GTARSKI1:def 17;
then Line (y,q) = Line (y,c) by A34, A20, GTARSKI3:82, A35, LemmaA1;
then A37: Line (q,(reflection (z,q))) = Line (y,c) by A22, A34, GTARSKI3:82, a32, LemmaA1;
Middle q,z, reflection (z,q) by GTARSKI3:def 13;
then between q,z, reflection (z,q) by GTARSKI3:def 12;
then Collinear q,z, reflection (z,q) by GTARSKI1:def 17;
then Collinear q, reflection (z,q),z by GTARSKI3:45;
then z in Line (y,c) by A37, LemmaA1;
then Collinear z,y,c by LemmaA2;
then c in Line (y,z) by LemmaA1;
then Collinear c,a,b by LemmaA2, A30;
hence contradiction by A1, GTARSKI3:45; :: thesis: verum

end;

take x ; :: thesis: x is_foot a,b,c

now :: thesis: ( are_orthogonal a,b,c,x & Collinear a,b,x )

now :: thesis: ( Line (y,z) is_line & Line (c,x) is_line & x in Line (y,z) & x in Line (c,x) & ex u, v being POINT of S st
( u in Line (y,z) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) )

thus Line (y,z) is_line by A21, GTARSKI3:def 11; :: thesis: ( Line (c,x) is_line & x in Line (y,z) & x in Line (c,x) & ex u, v being POINT of S st
( u in Line (y,z) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) )
thus Line (c,x) is_line by A31, GTARSKI3:def 11; :: thesis: ( x in Line (y,z) & x in Line (c,x) & ex u, v being POINT of S st
( u in Line (y,z) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) )
thus x in Line (y,z) by LemmaA1, A19; :: thesis: ( x in Line (c,x) & ex u, v being POINT of S st
( u in Line (y,z) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) )
thus x in Line (c,x) by GTARSKI3:83; :: thesis: ex u, v being POINT of S st
( u in Line (y,z) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v )
thus ex u, v being POINT of S st
( u in Line (y,z) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) :: thesis: verum

proof

take y ; :: thesis: ex v being POINT of S st
( y in Line (y,z) & v in Line (c,x) & y <> x & v <> x & right_angle y,x,v )
take c ; :: thesis: ( y in Line (y,z) & c in Line (c,x) & y <> x & c <> x & right_angle y,x,c )
thus y in Line (y,z) by GTARSKI3:83; :: thesis: ( c in Line (c,x) & y <> x & c <> x & right_angle y,x,c )
thus c in Line (c,x) by GTARSKI3:83; :: thesis: ( y <> x & c <> x & right_angle y,x,c )
thus y <> x by Satz8p18Lemma, A1, A2, A13, A7, A18, A17, A20, A10, A4, A8, A22, A6; :: thesis: ( c <> x & right_angle y,x,c )
thus c <> x by A31; :: thesis: right_angle y,x,c
thus right_angle y,x,c by A16, A17, GTARSKI3:def 13; :: thesis: verum

end;

end;

then are_orthogonal Line (a,b), Line (c,x) by A30, Satz8p13;
hence are_orthogonal a,b,c,x by GTARSKI3:46, A1, A31; :: thesis: Collinear a,b,x
x in Line (y,z) by LemmaA1, A19;
then Collinear x,a,b by LemmaA2, A30;
hence Collinear a,b,x by GTARSKI3:45; :: thesis: verum

end;

hence x is_foot a,b,c ; :: thesis: verum