let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 & c,a2 <= c,a1 holds
between m1,c,m2
let c, a1, a2, b1, b2, m1, m2 be POINT of S; ( between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 & c,a2 <= c,a1 implies between m1,c,m2 )
assume that
A1:
between a1,c,a2
and
A2:
between b1,c,b2
and
A3:
c,a1 equiv c,b1
and
A4:
c,a2 equiv c,b2
and
A5:
Middle a1,m1,b1
and
A6:
Middle a2,m2,b2
and
A7:
c,a2 <= c,a1
; between m1,c,m2
per cases
( a1 = c or a1 <> c )
;
suppose A8:
a1 = c
;
between m1,c,m2
a2 = c
then
(
Middle a1,
m1,
a1 &
Middle a2,
m2,
a2 )
by A5, A6, A8, A3, A4, Satz2p2, GTARSKI1:def 7;
then
(
m1 = a1 &
m2 = a2 )
by GTARSKI1:def 10;
hence
between m1,
c,
m2
by A8, Satz3p1, Satz3p2;
verum end; suppose A11:
a1 <> c
;
between m1,c,m2set a =
reflection (
c,
a1);
set b =
reflection (
c,
b1);
set m =
reflection (
c,
m1);
now ( c,a2 equiv c,a2 & c,a1 equiv c, reflection (c,a1) )thus
c,
a2 equiv c,
a2
by Satz2p1;
c,a1 equiv c, reflection (c,a1)
c,
a1 equiv reflection (
c,
c),
reflection (
c,
a1)
by Satz7p13;
hence
c,
a1 equiv c,
reflection (
c,
a1)
by Satz7p10;
verum end; then A12:
c,
a2 <= c,
reflection (
c,
a1)
by A7, Satz5p6;
per cases
( a2 = c or a2 <> c )
;
suppose A14:
a2 <> c
;
between m1,c,m2A15:
between c,
a2,
reflection (
c,
a1)
proof
c out a2,
reflection (
c,
a1)
proof
now ( c <> a2 & c <> reflection (c,a1) & ( between c,a2, reflection (c,a1) or between c, reflection (c,a1),a2 ) )thus
c <> a2
by A14;
( c <> reflection (c,a1) & ( between c,a2, reflection (c,a1) or between c, reflection (c,a1),a2 ) )thus
c <> reflection (
c,
a1)
( between c,a2, reflection (c,a1) or between c, reflection (c,a1),a2 )thus
(
between c,
a2,
reflection (
c,
a1) or
between c,
reflection (
c,
a1),
a2 )
verumproof
A16:
Middle a1,
c,
reflection (
c,
a1)
by DEFR;
then
(
between a1,
reflection (
c,
a1),
a2 or
between a1,
a2,
reflection (
c,
a1) )
by A1, A11, Satz5p1;
hence
(
between c,
a2,
reflection (
c,
a1) or
between c,
reflection (
c,
a1),
a2 )
by A1, A16, Satz3p6p1;
verum
end; end;
hence
c out a2,
reflection (
c,
a1)
;
verum
end;
hence
between c,
a2,
reflection (
c,
a1)
by A12, Satz6p13;
verum
end; A17:
between c,
b2,
reflection (
c,
b1)
proof
per cases
( c = b2 or c <> b2 )
;
suppose A18:
c <> b2
;
between c,b2, reflection (c,b1)A19:
c,
b2 <= c,
b1
by A3, A4, A7, Satz5p6;
c,
b1 equiv reflection (
c,
c),
reflection (
c,
b1)
by Satz7p13;
then
(
c,
b1 equiv c,
reflection (
c,
b1) &
c,
b2 equiv c,
b2 )
by Satz2p1, Satz7p10;
then A20:
c,
b2 <= c,
reflection (
c,
b1)
by A19, Satz5p6;
A21:
b1 <> c
by A11, A3, GTARSKI1:def 7;
c out b2,
reflection (
c,
b1)
proof
now ( c <> b2 & c <> reflection (c,b1) & ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 ) )thus
c <> b2
by A18;
( c <> reflection (c,b1) & ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 ) )thus
c <> reflection (
c,
b1)
( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 )thus
(
between c,
b2,
reflection (
c,
b1) or
between c,
reflection (
c,
b1),
b2 )
verum end;
hence
c out b2,
reflection (
c,
b1)
;
verum
end; hence
between c,
b2,
reflection (
c,
b1)
by A20, Satz6p13;
verum end; end;
end;
(
between reflection (
c,
a1),
a2,
c &
between reflection (
c,
b1),
b2,
c &
between reflection (
c,
a1),
reflection (
c,
m1),
reflection (
c,
b1) )
by A5, Satz7p15, A15, Satz3p2, A17;
then consider q being
POINT of
S such that A23:
between reflection (
c,
m1),
q,
c
and A24:
between a2,
q,
b2
by Satz3p17;
A25:
between reflection (
c,
m1),
c,
m1
q = m2
proof
reflection (
c,
a1),
a2,
c,
reflection (
c,
m1)
IFS reflection (
c,
b1),
b2,
c,
reflection (
c,
m1)
proof
now ( between reflection (c,a1),a2,c & between reflection (c,b1),b2,c & reflection (c,a1),c equiv reflection (c,b1),c & a2,c equiv b2,c & reflection (c,a1), reflection (c,m1) equiv reflection (c,b1), reflection (c,m1) & c, reflection (c,m1) equiv c, reflection (c,m1) )thus
between reflection (
c,
a1),
a2,
c
by A15, Satz3p2;
( between reflection (c,b1),b2,c & reflection (c,a1),c equiv reflection (c,b1),c & a2,c equiv b2,c & reflection (c,a1), reflection (c,m1) equiv reflection (c,b1), reflection (c,m1) & c, reflection (c,m1) equiv c, reflection (c,m1) )thus
between reflection (
c,
b1),
b2,
c
by A17, Satz3p2;
( reflection (c,a1),c equiv reflection (c,b1),c & a2,c equiv b2,c & reflection (c,a1), reflection (c,m1) equiv reflection (c,b1), reflection (c,m1) & c, reflection (c,m1) equiv c, reflection (c,m1) )
reflection (
c,
c),
reflection (
c,
a1)
equiv reflection (
c,
c),
reflection (
c,
b1)
by A3, Satz7p16;
then
c,
reflection (
c,
a1)
equiv reflection (
c,
c),
reflection (
c,
b1)
by Satz7p10;
then
c,
reflection (
c,
a1)
equiv c,
reflection (
c,
b1)
by Satz7p10;
then
c,
reflection (
c,
a1)
equiv reflection (
c,
b1),
c
by Satz2p5;
hence
reflection (
c,
a1),
c equiv reflection (
c,
b1),
c
by Satz2p4;
( a2,c equiv b2,c & reflection (c,a1), reflection (c,m1) equiv reflection (c,b1), reflection (c,m1) & c, reflection (c,m1) equiv c, reflection (c,m1) )
c,
a2 equiv b2,
c
by A4, Satz2p5;
hence
a2,
c equiv b2,
c
by Satz2p4;
( reflection (c,a1), reflection (c,m1) equiv reflection (c,b1), reflection (c,m1) & c, reflection (c,m1) equiv c, reflection (c,m1) )
m1,
a1 equiv b1,
m1
by A5, Satz2p5;
then
a1,
m1 equiv b1,
m1
by Satz2p4;
hence
reflection (
c,
a1),
reflection (
c,
m1)
equiv reflection (
c,
b1),
reflection (
c,
m1)
by Satz7p16;
c, reflection (c,m1) equiv c, reflection (c,m1)thus
c,
reflection (
c,
m1)
equiv c,
reflection (
c,
m1)
by Satz2p1;
verum end;
hence
reflection (
c,
a1),
a2,
c,
reflection (
c,
m1)
IFS reflection (
c,
b1),
b2,
c,
reflection (
c,
m1)
;
verum
end;
then
a2,
reflection (
c,
m1)
equiv b2,
reflection (
c,
m1)
by Satz4p2;
then A26:
a2,
reflection (
c,
m1)
equiv reflection (
c,
m1),
b2
by Satz2p5;
then A27:
reflection (
c,
m1),
a2 equiv reflection (
c,
m1),
b2
by Satz2p4;
q,
a2 equiv q,
b2
then
Middle a2,
q,
b2
by A24;
hence
q = m2
by A6, Satz7p17;
verum
end; then
between m2,
c,
m1
by A25, A23, Satz3p6p1;
hence
between m1,
c,
m2
by Satz3p2;
verum end; end; end; end;