let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: between m1,c,m2

per cases ( a1 = c or a1 <> c ) ;

suppose A8: a1 = c ; :: thesis: between m1,c,m2

a2 = c

proof

consider x being POINT of S such that
A9: between c,a2,x and
A10: c,x equiv c,c by A7, A8, Satz5p5;
c = x by A10, GTARSKI1:def 7;
hence a2 = c by A9, GTARSKI1:def 10; :: thesis: verum

end;

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; :: thesis: verum

end;

suppose A11: a1 <> c ; :: thesis: between m1,c,m2

set a = reflection (c,a1);
set b = reflection (c,b1);
set m = reflection (c,m1);

now :: thesis: ( c,a2 equiv c,a2 & c,a1 equiv c, reflection (c,a1) )

thus c,a2 equiv c,a2 by Satz2p1; :: thesis: 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; :: thesis: verum

end;

then A12: c,a2 <= c, reflection (c,a1) by A7, Satz5p6;

per cases ( a2 = c or a2 <> c ) ;

suppose A13: a2 = c ; :: thesis: between m1,c,m2

then a2 = b2 by A4, Satz2p2, GTARSKI1:def 7;
then m2 = a2 by A6, GTARSKI1:def 10;
hence between m1,c,m2 by A13, Satz3p1; :: thesis: verum

end;

suppose A14: a2 <> c ; :: thesis: between m1,c,m2

A15: between c,a2, reflection (c,a1)

proof

c out a2, reflection (c,a1)

proof

now :: thesis: ( c <> a2 & c <> reflection (c,a1) & ( between c,a2, reflection (c,a1) or between c, reflection (c,a1),a2 ) )

thus c <> a2 by A14; :: thesis: ( c <> reflection (c,a1) & ( between c,a2, reflection (c,a1) or between c, reflection (c,a1),a2 ) )
thus c <> reflection (c,a1) :: thesis: ( between c,a2, reflection (c,a1) or between c, reflection (c,a1),a2 )

proof

assume c = reflection (c,a1) ; :: thesis: contradiction
then reflection (c,a1) = reflection (c,c) by Satz7p10;
hence contradiction by A11, Satz7p9; :: thesis: verum

end;

thus ( between c,a2, reflection (c,a1) or between c, reflection (c,a1),a2 ) :: thesis: verum

proof

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; :: thesis: verum

end;

end;

hence c out a2, reflection (c,a1) ; :: thesis: verum

end;

hence between c,a2, reflection (c,a1) by A12, Satz6p13; :: thesis: verum

end;

A17: between c,b2, reflection (c,b1)

proof

per cases ( c = b2 or c <> b2 ) ;

suppose c = b2 ; :: thesis: between c,b2, reflection (c,b1)

hence between c,b2, reflection (c,b1) by A14, A4, GTARSKI1:def 7; :: thesis: verum

end;

suppose A18: c <> b2 ; :: thesis: 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 :: thesis: ( c <> b2 & c <> reflection (c,b1) & ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 ) )

thus c <> b2 by A18; :: thesis: ( c <> reflection (c,b1) & ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 ) )
thus c <> reflection (c,b1) :: thesis: ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 )

proof

assume c = reflection (c,b1) ; :: thesis: contradiction
then reflection (c,b1) = reflection (c,c) by Satz7p10;
hence contradiction by A21, Satz7p9; :: thesis: verum

end;

thus ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 ) :: thesis: verum

proof

A22: Middle b1,c, reflection (c,b1) by DEFR;

per cases then ( between b1, reflection (c,b1),b2 or between b1,b2, reflection (c,b1) ) by A2, A21, Satz5p1;

suppose between b1, reflection (c,b1),b2 ; :: thesis: ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 )

hence ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 ) by A22, Satz3p6p1; :: thesis: verum

end;

suppose between b1,b2, reflection (c,b1) ; :: thesis: ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 )

hence ( between c,b2, reflection (c,b1) or between c, reflection (c,b1),b2 ) by A2, Satz3p6p1; :: thesis: verum

end;

end;

end;

end;

hence c out b2, reflection (c,b1) ; :: thesis: verum

end;

hence between c,b2, reflection (c,b1) by A20, Satz6p13; :: thesis: 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

proof

Middle m1,c, reflection (c,m1) by DEFR;
hence between reflection (c,m1),c,m1 by Satz3p2; :: thesis: verum

end;

q = m2

proof

reflection (c,a1),a2,c, reflection (c,m1) IFS reflection (c,b1),b2,c, reflection (c,m1)

proof

now :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: ( 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; :: thesis: c, reflection (c,m1) equiv c, reflection (c,m1)
thus c, reflection (c,m1) equiv c, reflection (c,m1) by Satz2p1; :: thesis: verum

end;

hence reflection (c,a1),a2,c, reflection (c,m1) IFS reflection (c,b1),b2,c, reflection (c,m1) ; :: thesis: 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

proof

per cases ( reflection (c,m1) <> c or reflection (c,m1) = c ) ;

suppose A28: reflection (c,m1) <> c ; :: thesis: q,a2 equiv q,b2

Collinear c, reflection (c,m1),q by A23;
hence q,a2 equiv q,b2 by A4, A27, A28, Satz4p17; :: thesis: verum

end;

suppose reflection (c,m1) = c ; :: thesis: q,a2 equiv q,b2

then q = reflection (c,m1) by A23, GTARSKI1:def 10;
hence q,a2 equiv q,b2 by A26, Satz2p4; :: thesis: verum

end;

end;

end;

then Middle a2,q,b2 by A24;
hence q = m2 by A6, Satz7p17; :: thesis: verum

end;

then between m2,c,m1 by A25, A23, Satz3p6p1;
hence between m1,c,m2 by Satz3p2; :: thesis: verum

end;

end;

end;

end;