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,a1 <= c,a2 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,a1 <= c,a2 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,a1 <= c,a2 ; :: thesis: between m1,c,m2
per cases ( a2 = c or a2 <> c ) ;
suppose A8: a2 = c ; :: thesis: between m1,c,m2
a1 = c
proof
consider x being POINT of S such that
A9: between c,a1,x and
A10: c,x equiv c,c by A7, A8, Satz5p5;
c = x by A10, GTARSKI1:def 7;
hence a1 = 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; :: thesis: verum
end;
suppose A11: a2 <> c ; :: thesis: between m1,c,m2
set a = reflection (c,a2);
set b = reflection (c,b2);
set m = reflection (c,m2);
now :: thesis: ( c,a1 equiv c,a1 & c,a2 equiv c, reflection (c,a2) )
thus c,a1 equiv c,a1 by Satz2p1; :: thesis: c,a2 equiv c, reflection (c,a2)
c,a2 equiv reflection (c,c), reflection (c,a2) by Satz7p13;
hence c,a2 equiv c, reflection (c,a2) by Satz7p10; :: thesis: verum
end;
then A12: c,a1 <= c, reflection (c,a2) by A7, Satz5p6;
per cases ( a1 = c or a1 <> c ) ;
suppose A14: a1 <> c ; :: thesis: between m1,c,m2
A15: between c,a1, reflection (c,a2)
proof
c out a1, reflection (c,a2)
proof
now :: thesis: ( c <> a1 & c <> reflection (c,a2) & ( between c,a1, reflection (c,a2) or between c, reflection (c,a2),a1 ) )
thus c <> a1 by A14; :: thesis: ( c <> reflection (c,a2) & ( between c,a1, reflection (c,a2) or between c, reflection (c,a2),a1 ) )
thus c <> reflection (c,a2) :: thesis: ( between c,a1, reflection (c,a2) or between c, reflection (c,a2),a1 )
proof
assume c = reflection (c,a2) ; :: thesis: contradiction
then reflection (c,a2) = reflection (c,c) by Satz7p10;
hence contradiction by A11, Satz7p9; :: thesis: verum
end;
thus ( between c,a1, reflection (c,a2) or between c, reflection (c,a2),a1 ) :: thesis: verum
proof
A16: Middle a2,c, reflection (c,a2) by DEFR;
A17: between a2,c,a1 by A1, Satz3p2;
per cases then ( between a2, reflection (c,a2),a1 or between a2,a1, reflection (c,a2) ) by A11, A16, Satz5p1;
suppose between a2, reflection (c,a2),a1 ; :: thesis: ( between c,a1, reflection (c,a2) or between c, reflection (c,a2),a1 )
hence ( between c,a1, reflection (c,a2) or between c, reflection (c,a2),a1 ) by A16, Satz3p6p1; :: thesis: verum
end;
suppose between a2,a1, reflection (c,a2) ; :: thesis: ( between c,a1, reflection (c,a2) or between c, reflection (c,a2),a1 )
hence ( between c,a1, reflection (c,a2) or between c, reflection (c,a2),a1 ) by A17, Satz3p6p1; :: thesis: verum
end;
end;
end;
end;
hence c out a1, reflection (c,a2) ; :: thesis: verum
end;
hence between c,a1, reflection (c,a2) by A12, Satz6p13; :: thesis: verum
end;
A18: between c,b1, reflection (c,b2)
proof
per cases ( c = b1 or c <> b1 ) ;
suppose A19: c <> b1 ; :: thesis: between c,b1, reflection (c,b2)
A20: c,b1 <= c,b2 by A3, A4, A7, Satz5p6;
c,b2 equiv reflection (c,c), reflection (c,b2) by Satz7p13;
then ( c,b2 equiv c, reflection (c,b2) & c,b1 equiv c,b1 ) by Satz2p1, Satz7p10;
then A21: c,b1 <= c, reflection (c,b2) by A20, Satz5p6;
A22: b2 <> c by A11, A4, GTARSKI1:def 7;
c out b1, reflection (c,b2)
proof
now :: thesis: ( c <> b1 & c <> reflection (c,b2) & ( between c,b1, reflection (c,b2) or between c, reflection (c,b2),b1 ) )
thus c <> b1 by A19; :: thesis: ( c <> reflection (c,b2) & ( between c,b1, reflection (c,b2) or between c, reflection (c,b2),b1 ) )
thus c <> reflection (c,b2) :: thesis: ( between c,b1, reflection (c,b2) or between c, reflection (c,b2),b1 )
proof
assume c = reflection (c,b2) ; :: thesis: contradiction
then reflection (c,b2) = reflection (c,c) by Satz7p10;
hence contradiction by A22, Satz7p9; :: thesis: verum
end;
thus ( between c,b1, reflection (c,b2) or between c, reflection (c,b2),b1 ) :: thesis: verum
proof
A23: Middle b2,c, reflection (c,b2) by DEFR;
A24: between b2,c,b1 by A2, Satz3p2;
then ( between b2, reflection (c,b2),b1 or between b2,b1, reflection (c,b2) ) by A22, A23, Satz5p1;
hence ( between c,b1, reflection (c,b2) or between c, reflection (c,b2),b1 ) by A23, A24, Satz3p6p1; :: thesis: verum
end;
end;
hence c out b1, reflection (c,b2) ; :: thesis: verum
end;
hence between c,b1, reflection (c,b2) by A21, Satz6p13; :: thesis: verum
end;
end;
end;
( between reflection (c,a2),a1,c & between reflection (c,b2),b1,c & between reflection (c,a2), reflection (c,m2), reflection (c,b2) ) by A18, Satz3p2, A15, A6, Satz7p15;
then consider q being POINT of S such that
A25: between reflection (c,m2),q,c and
A26: between a1,q,b1 by Satz3p17;
A27: between reflection (c,m2),c,m2
proof
Middle m2,c, reflection (c,m2) by DEFR;
hence between reflection (c,m2),c,m2 by Satz3p2; :: thesis: verum
end;
q = m1
proof
reflection (c,a2),a1,c, reflection (c,m2) IFS reflection (c,b2),b1,c, reflection (c,m2)
proof
now :: thesis: ( between reflection (c,a2),a1,c & between reflection (c,b2),b1,c & reflection (c,a2),c equiv reflection (c,b2),c & a1,c equiv b1,c & reflection (c,a2), reflection (c,m2) equiv reflection (c,b2), reflection (c,m2) & c, reflection (c,m2) equiv c, reflection (c,m2) )
thus between reflection (c,a2),a1,c by A15, Satz3p2; :: thesis: ( between reflection (c,b2),b1,c & reflection (c,a2),c equiv reflection (c,b2),c & a1,c equiv b1,c & reflection (c,a2), reflection (c,m2) equiv reflection (c,b2), reflection (c,m2) & c, reflection (c,m2) equiv c, reflection (c,m2) )
thus between reflection (c,b2),b1,c by A18, Satz3p2; :: thesis: ( reflection (c,a2),c equiv reflection (c,b2),c & a1,c equiv b1,c & reflection (c,a2), reflection (c,m2) equiv reflection (c,b2), reflection (c,m2) & c, reflection (c,m2) equiv c, reflection (c,m2) )
reflection (c,c), reflection (c,a2) equiv reflection (c,c), reflection (c,b2) by A4, Satz7p16;
then c, reflection (c,a2) equiv reflection (c,c), reflection (c,b2) by Satz7p10;
then c, reflection (c,a2) equiv c, reflection (c,b2) by Satz7p10;
then c, reflection (c,a2) equiv reflection (c,b2),c by Satz2p5;
hence reflection (c,a2),c equiv reflection (c,b2),c by Satz2p4; :: thesis: ( a1,c equiv b1,c & reflection (c,a2), reflection (c,m2) equiv reflection (c,b2), reflection (c,m2) & c, reflection (c,m2) equiv c, reflection (c,m2) )
c,a1 equiv b1,c by A3, Satz2p5;
hence a1,c equiv b1,c by Satz2p4; :: thesis: ( reflection (c,a2), reflection (c,m2) equiv reflection (c,b2), reflection (c,m2) & c, reflection (c,m2) equiv c, reflection (c,m2) )
m2,a2 equiv b2,m2 by A6, Satz2p5;
then a2,m2 equiv b2,m2 by Satz2p4;
hence reflection (c,a2), reflection (c,m2) equiv reflection (c,b2), reflection (c,m2) by Satz7p16; :: thesis: c, reflection (c,m2) equiv c, reflection (c,m2)
thus c, reflection (c,m2) equiv c, reflection (c,m2) by Satz2p1; :: thesis: verum
end;
hence reflection (c,a2),a1,c, reflection (c,m2) IFS reflection (c,b2),b1,c, reflection (c,m2) ; :: thesis: verum
end;
then a1, reflection (c,m2) equiv b1, reflection (c,m2) by Satz4p2;
then A28: a1, reflection (c,m2) equiv reflection (c,m2),b1 by Satz2p5;
then A29: reflection (c,m2),a1 equiv reflection (c,m2),b1 by Satz2p4;
q,a1 equiv q,b1
proof
per cases ( reflection (c,m2) <> c or reflection (c,m2) = c ) ;
suppose A30: reflection (c,m2) <> c ; :: thesis: q,a1 equiv q,b1
Collinear c, reflection (c,m2),q by A25;
hence q,a1 equiv q,b1 by A3, A29, A30, Satz4p17; :: thesis: verum
end;
end;
end;
then Middle a1,q,b1 by A26;
hence q = m1 by A5, Satz7p17; :: thesis: verum
end;
hence between m1,c,m2 by A27, A25, Satz3p6p1; :: thesis: verum
end;
end;
end;
end;