let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, c, m, r, s being POINT of S
for A being Subset of S st between a,A,c & r in A & are_orthogonal A,r,a & s in A & are_orthogonal A,s,c holds
( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )
let a, c, m, r, s be POINT of S; :: thesis: for A being Subset of S st between a,A,c & r in A & are_orthogonal A,r,a & s in A & are_orthogonal A,s,c holds
( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )
let A be Subset of S; :: thesis: ( between a,A,c & r in A & are_orthogonal A,r,a & s in A & are_orthogonal A,s,c implies ( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) ) )
assume that
A1: between a,A,c and
A2: r in A and
A3: are_orthogonal A,r,a and
A4: s in A and
A5: are_orthogonal A,s,c ; :: thesis: ( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )
consider t being POINT of S such that
A6: t in A and
A7: between a,t,c by A1;
( a <> r & are_orthogonal A,r, Line (r,a) ) by A3, GTARSKI4:def 4;
then A8: right_angle t,r,a by A6, GTARSKI3:83;
( c <> s & are_orthogonal A,s, Line (s,c) ) by A5, GTARSKI4:def 4;
then A10: right_angle t,s,c by A6, GTARSKI3:83;

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

suppose A11: r <> s ; :: thesis: ( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )

per cases ( r,a <= s,c or s,c <= r,a ) by GTARSKI3:64;

suppose A12: r,a <= s,c ; :: thesis: ( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )

A13: between c,A,a by A1, GTARSKI3:14;
then A14: ( ( Middle s,m,r implies for u being POINT of S holds
( s out u,c iff r out reflection (m,u),a ) ) & ( for u, v being POINT of S st s out u,c & r out v,a holds
between u,A,v ) ) by A12, A11, A2, A3, A4, A5, Th9;

now :: thesis: ( ( Middle r,m,s implies for u being POINT of S holds
( ( r out u,a implies s out reflection (m,u),c ) & ( s out reflection (m,u),c implies r out u,a ) ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )

hereby :: thesis: for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v

assume A15: Middle r,m,s ; :: thesis: for u being POINT of S holds
( ( r out u,a implies s out reflection (m,u),c ) & ( s out reflection (m,u),c implies r out u,a ) )
let u be POINT of S; :: thesis: ( ( r out u,a implies s out reflection (m,u),c ) & ( s out reflection (m,u),c implies r out u,a ) )

hereby :: thesis: ( s out reflection (m,u),c implies r out u,a )

assume r out u,a ; :: thesis: s out reflection (m,u),c
then r out reflection (m,(reflection (m,u))),a by GTARSKI3:101;
hence s out reflection (m,u),c by A15, A14, GTARSKI3:96; :: thesis: verum

end;

assume s out reflection (m,u),c ; :: thesis: r out u,a
then r out reflection (m,(reflection (m,u))),a by A14, A15, GTARSKI3:96;
hence r out u,a by GTARSKI3:101; :: thesis: verum

end;

let u, v be POINT of S; :: thesis: ( r out u,a & s out v,c implies between u,A,v )
assume ( r out u,a & s out v,c ) ; :: thesis: between u,A,v
then between v,A,u by A13, A12, A11, A2, A3, A4, A5, Th9;
hence between u,A,v by GTARSKI3:14; :: thesis: verum

end;

hence ( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) ) ; :: thesis: verum

end;

suppose s,c <= r,a ; :: thesis: ( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )

hence ( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) ) by A11, A1, A2, A3, A4, A5, Th9; :: thesis: verum

end;

end;

end;

suppose A18: r = s ; :: thesis: ( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )

A19: ( right_angle a,r,t & right_angle c,s,t ) by A8, A10, GTARSKI4:13;
then A20: r = t by A7, A18, GTARSKI4:18;
A21: between a,r,c by A19, A7, A18, GTARSKI4:18;

A22: now :: thesis: ( Middle r,m,s implies for u being POINT of S holds
( ( r out u,a implies s out reflection (m,u),c ) & ( s out reflection (m,u),c implies r out u,a ) ) )

assume A23: Middle r,m,s ; :: thesis: for u being POINT of S holds
( ( r out u,a implies s out reflection (m,u),c ) & ( s out reflection (m,u),c implies r out u,a ) )
then A24: ( r = m & m = s ) by A18, GTARSKI3:97;
let u be POINT of S; :: thesis: ( ( r out u,a implies s out reflection (m,u),c ) & ( s out reflection (m,u),c implies r out u,a ) )

hereby :: thesis: ( s out reflection (m,u),c implies r out u,a )

assume A25: r out u,a ; :: thesis: s out reflection (m,u),c
T1: m <> reflection (m,u)

proof

assume m = reflection (m,u) ; :: thesis: contradiction
then Middle u,m,m by GTARSKI3:def 13;
hence contradiction by A25, A24, GTARSKI1:def 7; :: thesis: verum

end;

( between m, reflection (m,u),c or between m,c, reflection (m,u) )

proof

per cases ( between r,u,a or between r,a,u ) by A25;

suppose A26: between r,u,a ; :: thesis: ( between m, reflection (m,u),c or between m,c, reflection (m,u) )

( between a,u,m & between a,m,c ) by A26, A24, A7, GTARSKI3:14, A19, GTARSKI4:18;
then G1: between u,m,c by GTARSKI3:18;
g2: Middle u,m, reflection (m,u) by GTARSKI3:def 13;
u <> m by A23, A18, GTARSKI3:97, A25;
hence ( between m, reflection (m,u),c or between m,c, reflection (m,u) ) by G1, g2, GTARSKI3:57; :: thesis: verum

end;

suppose A27: between r,a,u ; :: thesis: ( between m, reflection (m,u),c or between m,c, reflection (m,u) )

( between m,a,u & between c,m,a & a <> m ) by A7, A27, A24, A20, GTARSKI3:14, A3, GTARSKI4:def 4;
then between c,m,u by GTARSKI3:19;
then G1: between u,m,c by GTARSKI3:14;
Middle u,m, reflection (m,u) by GTARSKI3:def 13;
then ( between u,m, reflection (m,u) & u <> m ) by A23, A18, GTARSKI3:97, A25;
hence ( between m, reflection (m,u),c or between m,c, reflection (m,u) ) by G1, GTARSKI3:57; :: thesis: verum

end;

end;

end;

hence s out reflection (m,u),c by T1, A5, GTARSKI4:def 4, A23, A18, GTARSKI3:97; :: thesis: verum

end;

assume A28: s out reflection (m,u),c ; :: thesis: r out u,a

now :: thesis: ( r <> u & r <> a & ( between r,u,a or between r,a,u ) )

thus ( r <> u & r <> a ) by A24, A28, GTARSKI3:104, A3, GTARSKI4:def 4; :: thesis: ( between r,u,a or between r,a,u )
Middle u,m, reflection (m,u) by GTARSKI3:def 13;
then between u,r,c by A24, A28, GTARSKI3:17, GTARSKI3:19;
then Y1: between c,r,u by GTARSKI3:14;
( between c,r,a & c <> r ) by A5, GTARSKI4:def 4, A18, A7, A20, GTARSKI3:14;
hence ( between r,u,a or between r,a,u ) by Y1, GTARSKI3:57; :: thesis: verum

end;

hence r out u,a ; :: thesis: verum

end;

for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v

proof

let u, v be POINT of S; :: thesis: ( r out u,a & s out v,c implies between u,A,v )
assume that
A29: r out u,a and
A30: s out v,c ; :: thesis: between u,A,v
( Collinear u,r,a or Collinear a,r,u ) by A29;
then A31: Collinear u,r,a by GTARSKI3:45;
( Collinear r,v,c or Collinear r,c,v ) by A18, A30;
then A32: Collinear v,r,c by GTARSKI3:45;
U1: ( not u in A & not v in A )

proof

assume ( u in A or v in A ) ; :: thesis: contradiction

per cases then ( u in A or v in A ) ;

suppose u in A ; :: thesis: contradiction

then Line (u,r) = A by A1, A29, A2, GTARSKI3:87;
hence contradiction by A1, A31; :: thesis: verum

end;

suppose v in A ; :: thesis: contradiction

then Line (v,r) = A by A2, A18, A1, A30, GTARSKI3:87;
hence contradiction by A32, A1; :: thesis: verum

end;

end;

end;

( between a,u,r or between u,a,r ) by A29, GTARSKI3:14;
then between u,r,v by Th8, A29, A30, A18, A21;
hence between u,A,v by A1, A2, U1; :: thesis: verum

end;

hence ( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) ) by A22; :: thesis: verum

end;

end;