let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; for a, c, r being POINT of S
for A being Subset of S st between a,A,c & r in A holds
for b being POINT of S st r out a,b holds
between b,A,c
let a, c, r be POINT of S; for A being Subset of S st between a,A,c & r in A holds
for b being POINT of S st r out a,b holds
between b,A,c
let A be Subset of S; ( between a,A,c & r in A implies for b being POINT of S st r out a,b holds
between b,A,c )
assume that
A1:
between a,A,c
and
A2:
r in A
; for b being POINT of S st r out a,b holds
between b,A,c
let b be POINT of S; ( r out a,b implies between b,A,c )
assume A3:
r out a,b
; between b,A,c
A is_line
by A1;
then consider p, q being POINT of S such that
p <> q
and
A4:
A = Line (p,q)
;
not Collinear p,q,a
by A1, A4;
then consider x being POINT of S such that
A5:
x is_foot p,q,a
by GTARSKI4:33;
A6:
x in A
by A4, A5;
A7:
not b in A
proof
assume
b in A
;
contradiction
then A8:
Line (
r,
b)
= A
by A3, A1, A2, GTARSKI3:87;
(
Collinear r,
a,
b or
Collinear r,
b,
a )
by A3;
then
Collinear r,
b,
a
by GTARSKI3:45;
hence
contradiction
by A8, A1;
verum
end;
then
not Collinear p,q,b
by A4;
then consider y being POINT of S such that
A9:
y is_foot p,q,b
by GTARSKI4:33;
A10:
y in A
by A4, A9;
not Collinear p,q,c
by A1, A4;
then consider z being POINT of S such that
A11:
z is_foot p,q,c
by GTARSKI4:33;
A12:
z in { x where x is POINT of S : Collinear p,q,x }
by A11;
A13:
z in A
by A4, A11;
consider m being POINT of S such that
A14:
Middle x,m,z
by GTARSKI4:39;
Collinear x,m,z
by A14;
then
Collinear x,z,m
by GTARSKI3:45;
then A15:
m in Line (x,z)
;
a16:
( x = z or x <> z )
;
then A16:
m in A
by A14, GTARSKI3:97, A13, A15, A6, A1, GTARSKI3:87;
set d = reflection (m,a);
A17:
not reflection (m,a) in A
proof
assume A18:
reflection (
m,
a)
in A
;
contradiction
Middle a,
m,
reflection (
m,
a)
by GTARSKI3:def 13;
then
Collinear m,
reflection (
m,
a),
a
;
then A19:
a in Line (
m,
(reflection (m,a)))
;
m <> reflection (
m,
a)
hence
contradiction
by A18, A16, A1, A19, GTARSKI3:87;
verum
end;
A20:
z <> reflection (m,a)
proof
assume A21:
z = reflection (
m,
a)
;
contradiction
then
Middle a,
m,
z
by GTARSKI3:def 13;
then
Collinear a,
m,
z
;
then
Collinear z,
m,
a
by GTARSKI3:45;
then A22:
a in Line (
z,
m)
;
(
Middle a,
m,
m or
z <> m )
by A21, GTARSKI3:def 13;
hence
contradiction
by A16, GTARSKI1:def 7, A22, A1, A12, A4, GTARSKI3:87;
verum
end;
J2:
x in A
by A5, A4;
yh1:
( Collinear p,q,x & are_orthogonal p,q,a,x )
by A5;
( A is_line & Line (x,a) is_line & A <> Line (x,a) & x in Line (x,a) & x in A )
by A1, A6, GTARSKI3:83;
then
A, Line (x,a) Is x
;
then J3:
are_orthogonal A,x,a
by yh1, A4, GTARSKI4:26, GTARSKI4:def 4;
J4:
z in A
by A11, A4;
y1:
( Collinear p,q,z & are_orthogonal p,q,c,z )
by A11;
( A is_line & Line (z,c) is_line & A <> Line (z,c) & z in Line (z,c) & z in A )
by A1, A13, GTARSKI3:83;
then
A, Line (z,c) Is z
;
then J5:
are_orthogonal A,z,c
by y1, A4, GTARSKI4:26, GTARSKI4:def 4;
J6:
( Middle x,m,z & x out a,a )
by A5, A4, A1, A14, GTARSKI3:13;
then A24:
z out reflection (m,a),c
by A1, J2, J3, J4, J5, Th10;
( between a,A, reflection (m,a) & m in A & Middle a,m, reflection (m,a) & r in A & r out a,b )
by A3, A2, GTARSKI3:def 13, GTARSKI3:87, GTARSKI3:97, a16, A15, A24, A1, J2, J3, J4, J5, J6, Th10;
then T1:
between b,A, reflection (m,a)
by Th7;
T2:
y in A
by A9, A4;
g1:
( Collinear p,q,y & are_orthogonal p,q,b,y )
by A9;
( A is_line & Line (y,b) is_line & A <> Line (y,b) & y in Line (y,b) & y in A )
by A1, A10, A7, GTARSKI3:83;
then
A, Line (y,b) Is y
;
then T3:
are_orthogonal A,y,b
by g1, A4, GTARSKI4:def 4, GTARSKI4:26;
T4:
z in A
by A11, A4;
( Collinear z,c, reflection (m,a) or Collinear z, reflection (m,a),c )
by A24;
then
Collinear z,c, reflection (m,a)
by GTARSKI3:45;
then D1:
reflection (m,a) in Line (z,c)
;
( z <> c & Collinear p,q,z & are_orthogonal p,q,c,z )
by A11, A4, A1;
then D2:
are_orthogonal A, Line (z,(reflection (m,a)))
by D1, A4, A20, GTARSKI3:82;
( A is_line & Line (z,(reflection (m,a))) is_line & A <> Line (z,(reflection (m,a))) & z in Line (z,(reflection (m,a))) & z in A )
by A1, A17, A12, A4, GTARSKI3:83;
then
A, Line (z,(reflection (m,a))) Is z
;
then T5:
are_orthogonal A,z, reflection (m,a)
by A20, D2, GTARSKI4:26, GTARSKI4:def 4;
( y out b,b & z out c, reflection (m,a) )
by A24, A9, A4, A7, GTARSKI3:13;
hence
between b,A,c
by T1, T2, T3, T4, T5, Th10; verum