let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, p, q, t being POINT of S st a,p <= b,q & are_orthogonal a,b,q,b & are_orthogonal a,b,p,a & Collinear a,b,t & between q,t,p holds
ex x being POINT of S st Middle a,x,b
let a, b, p, q, t be POINT of S; :: thesis: ( a,p <= b,q & are_orthogonal a,b,q,b & are_orthogonal a,b,p,a & Collinear a,b,t & between q,t,p implies ex x being POINT of S st Middle a,x,b )
assume that
A1: a,p <= b,q and
A2: are_orthogonal a,b,q,b and
A3: are_orthogonal a,b,p,a and
A4: Collinear a,b,t and
A5: between q,t,p ; :: thesis: ex x being POINT of S st Middle a,x,b
consider r being POINT of S such that
A6: between b,r,q and
A7: a,p equiv b,r by A1, GTARSKI3:def 7;
between p,t,q by A5, GTARSKI3:14;
then consider x being POINT of S such that
A8: between t,x,b and
A9: between r,x,p by A6, GTARSKI1:def 11;
A10: Collinear a,b,x

proof

per cases ( b = t or b <> t ) ;

suppose b = t ; :: thesis: Collinear a,b,x

then x = b by A8, GTARSKI1:def 10;
then Collinear b,x,a by GTARSKI3:46;
hence Collinear a,b,x by GTARSKI3:45; :: thesis: verum

end;

suppose b <> t ; :: thesis: Collinear a,b,x

then A12: Line (t,b) = Line (a,b) by A2, GTARSKI3:82, A4, LemmaA1;
Collinear t,x,b by A8, GTARSKI1:def 17;
then Collinear t,b,x by GTARSKI3:45;
then x in Line (a,b) by A12, LemmaA1;
then Collinear x,a,b by LemmaA2;
hence Collinear a,b,x by GTARSKI3:45; :: thesis: verum

end;

end;

end;

( a <> b & q <> b & are_orthogonal Line (a,b), Line (q,b) ) by A2;
then consider x9 being POINT of S such that
A13: are_orthogonal Line (a,b),x9, Line (q,b) ;
( b in Line (a,b) & b in Line (q,b) ) by GTARSKI3:83;
then right_angle b,x9,b by A13;
then b = reflection (x9,b) by GTARSKI1:def 7, GTARSKI3:4;
then Middle b,x9,b by GTARSKI3:100;
then A14: x9 = b by GTARSKI3:97;
A15: ( a in Line (a,b) & q in Line (q,b) ) by GTARSKI3:83;
( a <> b & p <> a & are_orthogonal Line (a,b), Line (p,a) ) by A3;
then consider y being POINT of S such that
A16: are_orthogonal Line (a,b),y, Line (p,a) ;
A17: ( b in Line (a,b) & p in Line (p,a) ) by GTARSKI3:83;
then A18: right_angle b,y,p by A16;
( a in Line (a,b) & a in Line (p,a) ) by GTARSKI3:83;
then right_angle a,y,a by A16;
then a = reflection (y,a) by GTARSKI1:def 7, GTARSKI3:4;
then Middle a,y,a by GTARSKI3:100;
then A19: y = a by GTARSKI3:97;
( right_angle q,b,a & q <> b & Collinear b,q,r ) by A13, Satz8p2, A2, A6, A14, A15, Prelim08a;
then A20: right_angle r,b,a by Satz8p3;
A21: ( not Collinear b,a,p & not Collinear a,b,q ) by A3, A15, A14, A13, A17, A16, A19, A2, Satz8p9;
A22: r <> b by A3, A7, GTARSKI1:5;

now :: thesis: ( not Collinear a,p,b & p <> r & a,p equiv b,r & p,b equiv r,a & Collinear a,x,b & Collinear p,x,r )

thus not Collinear a,p,b by A21, GTARSKI3:45; :: thesis: ( p <> r & a,p equiv b,r & p,b equiv r,a & Collinear a,x,b & Collinear p,x,r )
thus p <> r :: thesis: ( a,p equiv b,r & p,b equiv r,a & Collinear a,x,b & Collinear p,x,r )

proof

assume A23: p = r ; :: thesis: contradiction
then p = x by A9, GTARSKI1:8;
then b = r by A20, A2, Satz8p9, A10, A23, Satz8p2;
hence contradiction by A23, A17, A19, A2, A16, Satz8p8; :: thesis: verum

end;

thus a,p equiv b,r by A7; :: thesis: ( p,b equiv r,a & Collinear a,x,b & Collinear p,x,r )
A24: x <> a

proof

assume x = a ; :: thesis: contradiction
then A25: Collinear r,a,p by A9, GTARSKI1:def 17;
right_angle a,b,r by A20, Satz8p2;
then not Collinear p,a,r by A3, A18, A19, Th01;
hence contradiction by A25, GTARSKI3:45; :: thesis: verum

end;

thus p,b equiv r,a :: thesis: ( Collinear a,x,b & Collinear p,x,r )

proof

set p9 = reflection (a,p);
consider r9 being POINT of S such that
A26: between reflection (a,p),x,r9 and
A27: x,r9 equiv x,r by GTARSKI1:def 8;
consider m being POINT of S such that
A28: Middle r9,m,r by A27, GTARSKI3:117;
A29: Middle r,m,r9 by A28, GTARSKI3:96;
A30: right_angle x,a,p by A17, A19, A10, A2, A16, Satz8p3;
A31: p <> reflection (a,p) by A3, LemmaA3;
Collinear p,a, reflection (a,p) by GTARSKI3:def 13, Prelim08;
then A32: Line (a,p) = Line (p,(reflection (a,p))) by A31, A3, Prelim07;
A33: not Collinear x,p, reflection (a,p)

proof

assume Collinear x,p, reflection (a,p) ; :: thesis: contradiction
then Collinear p, reflection (a,p),x by GTARSKI3:45;
then x in Line (a,p) by A32, LemmaA1;
hence contradiction by A30, A24, A3, Satz8p9, LemmaA2; :: thesis: verum

end;

( between reflection (a,p),x,r9 & between p,x,r & x, reflection (a,p) equiv x,p & x,r9 equiv x,r & Middle reflection (a,p),a,p & Middle r9,m,r ) by A9, GTARSKI3:14, A26, A28, A30, Prelim01, A27, GTARSKI3:96, GTARSKI3:def 13;
then A34: between a,x,m by GTARSKI3:115;
A35: x <> m

proof

assume A36: x = m ; :: thesis: contradiction
Collinear x,r9, reflection (a,p) by A26, Prelim08a;
then A37: reflection (a,p) in Line (x,r9) by LemmaA1;
A38: Collinear x,r,r9 by A36, A28, Prelim08a;

per cases ( x <> r or x = r ) ;

suppose A39: x <> r ; :: thesis: contradiction

then x <> r9 by A27, GTARSKI1:5, GTARSKI3:4;
then Line (x,r) = Line (x,r9) by A39, A38, Prelim07;
then Collinear reflection (a,p),x,r by A37, LemmaA2;
then A40: Collinear x,r, reflection (a,p) by GTARSKI3:45;
Collinear x,r,p by A9, Prelim08a;
hence contradiction by A33, A39, Prelim08b, A40; :: thesis: verum

end;

suppose x = r ; :: thesis: contradiction

hence contradiction by A20, A10, A2, A22, Satz8p2, Satz8p9; :: thesis: verum

end;

end;

end;

Collinear a,x,m by A34, GTARSKI1:def 17;
then A41: m in Line (a,x) by LemmaA1;
then A43: m in Line (a,b) by A24, A2, GTARSKI3:82, A10, LemmaA1;
A44: reflection (m,r) = r9 by A28, GTARSKI3:96, GTARSKI3:100;

now :: thesis: ( a <> b & r <> m & are_orthogonal Line (a,b), Line (r,m) )

thus a <> b by A2; :: thesis: ( r <> m & are_orthogonal Line (a,b), Line (r,m) )
thus A45: r <> m by A43, LemmaA2, A20, A2, A22, Satz8p9; :: thesis: are_orthogonal Line (a,b), Line (r,m)
thus are_orthogonal Line (a,b), Line (r,m) :: thesis: verum

proof

now :: thesis: ( Line (a,b) is_line & Line (r,m) is_line & m in Line (a,b) & m in Line (r,m) & ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v ) )

thus Line (a,b) is_line by A2, GTARSKI3:def 11; :: thesis: ( Line (r,m) is_line & m in Line (a,b) & m in Line (r,m) & ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v ) )
thus Line (r,m) is_line by A45, GTARSKI3:def 11; :: thesis: ( m in Line (a,b) & m in Line (r,m) & ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v ) )
thus m in Line (a,b) by A10, LemmaA1, A41, A24, A2, GTARSKI3:82; :: thesis: ( m in Line (r,m) & ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v ) )
thus m in Line (r,m) by GTARSKI3:83; :: thesis: ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v )
b3: x in Line (a,b) by A10, LemmaA1;
b4: r in Line (r,m) by GTARSKI3:83;
right_angle x,m,r by A44, GTARSKI3:4, A27;
hence ex u, v being POINT of S st
( u <> m & v <> m & u in Line (a,b) & v in Line (r,m) & right_angle u,m,v ) by A35, A45, b3, b4; :: thesis: verum

end;

hence are_orthogonal Line (a,b), Line (r,m) by Satz8p13; :: thesis: verum

end;

end;

then A46: are_orthogonal a,b,r,m ;
Collinear m,a,b by A43, LemmaA2;
then A47: m is_foot a,b,r by A46, GTARSKI3:45;

now :: thesis: ( Collinear a,b,b & are_orthogonal a,b,r,b )

thus Collinear a,b,b by Prelim05; :: thesis: are_orthogonal a,b,r,b
thus are_orthogonal a,b,r,b :: thesis: verum

proof

set A = Line (a,b);
set A9 = Line (r,b);

now :: thesis: ( Line (a,b) is_line & Line (r,b) is_line & b in Line (a,b) & b in Line (r,b) & ex u, v being POINT of S st
( u in Line (a,b) & v in Line (r,b) & u <> b & v <> b & right_angle u,b,v ) )

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

proof

take a ; :: thesis: ex v being POINT of S st
( a in Line (a,b) & v in Line (r,b) & a <> b & v <> b & right_angle a,b,v )
take r ; :: thesis: ( a in Line (a,b) & r in Line (r,b) & a <> b & r <> b & right_angle a,b,r )
thus a in Line (a,b) by GTARSKI3:83; :: thesis: ( r in Line (r,b) & a <> b & r <> b & right_angle a,b,r )
thus r in Line (r,b) by GTARSKI3:83; :: thesis: ( a <> b & r <> b & right_angle a,b,r )
thus a <> b by A2; :: thesis: ( r <> b & right_angle a,b,r )
thus r <> b by A3, A7, GTARSKI1:5; :: thesis: right_angle a,b,r
thus right_angle a,b,r by A20, Satz8p2; :: thesis: verum

end;

end;

then are_orthogonal Line (a,b), Line (r,b) by Satz8p13;
hence are_orthogonal a,b,r,b by A3, A7, GTARSKI1:5; :: thesis: verum

end;

end;

then A48: b is_foot a,b,r ;
then A49: m = b by A47, Satz8p18Uniqueness;
A50: Middle r,b,r9 by A29, A47, A48, Satz8p18Uniqueness;
A51: Middle p,a, reflection (a,p) by GTARSKI3:def 13;

now :: thesis: ( Middle reflection (a,p),a,p & between reflection (a,p),a,p & between r,b,r9 & reflection (a,p),p equiv r,r9 & a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )

thus A52: Middle reflection (a,p),a,p by GTARSKI3:96, GTARSKI3:def 13; :: thesis: ( between reflection (a,p),a,p & between r,b,r9 & reflection (a,p),p equiv r,r9 & a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )
hence between reflection (a,p),a,p by GTARSKI3:def 12; :: thesis: ( between r,b,r9 & reflection (a,p),p equiv r,r9 & a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )
thus between r,b,r9 by A50, GTARSKI3:def 12; :: thesis: ( reflection (a,p),p equiv r,r9 & a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )
A53: a,p equiv a, reflection (a,p) by A51, GTARSKI3:def 12;
A54: m,r9 equiv m,r by A28, GTARSKI3:def 12;
( between reflection (a,p),a,p & between r,m,r9 & reflection (a,p),a equiv r,m & a,p equiv m,r9 ) by A53, A29, GTARSKI3:def 12, A7, A54, A49, Prelim03, A52;
hence reflection (a,p),p equiv r,r9 by GTARSKI3:11; :: thesis: ( a,p equiv b,r9 & reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )
thus a,p equiv b,r9 by A7, A54, A49, Prelim03; :: thesis: ( reflection (a,p),r equiv r, reflection (a,p) & p,r equiv r9, reflection (a,p) )
reflection (a,p),r equiv reflection (a,p),r by GTARSKI3:1;
hence reflection (a,p),r equiv r, reflection (a,p) by Prelim01; :: thesis: p,r equiv r9, reflection (a,p)
( between p,x,r & between reflection (a,p),x,r9 & p,x equiv reflection (a,p),x & x,r equiv x,r9 ) by A26, A30, A9, GTARSKI3:14, Prelim01, A27;
then p,r equiv reflection (a,p),r9 by GTARSKI3:11;
hence p,r equiv r9, reflection (a,p) by Prelim01; :: thesis: verum

end;

then reflection (a,p),a,p,r IFS r,b,r9, reflection (a,p) by GTARSKI3:def 5;
then a,r equiv b, reflection (a,p) by GTARSKI3:41;
hence p,b equiv r,a by A18, A19, Prelim03; :: thesis: verum

end;

thus Collinear a,x,b by A10, GTARSKI3:45; :: thesis: Collinear p,x,r
Collinear r,x,p by A9, GTARSKI1:def 17;
hence Collinear p,x,r by GTARSKI3:45; :: thesis: verum

end;

then ( Middle a,x,b & Middle p,x,r ) by GTARSKI3:112;
hence ex x being POINT of S st Middle a,x,b ; :: thesis: verum