let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, p, p9 being POINT of S st Middle p,a,p9 & Middle p,b,p9 holds
a = b
let a, b, p, p9 be POINT of S; :: thesis: ( Middle p,a,p9 & Middle p,b,p9 implies a = b )
assume that
A1: Middle p,a,p9 and
A2: Middle p,b,p9 ; :: thesis: a = b
now :: thesis: ( between p,b,p9 & p,b equiv reflection (a,b),p & p,b equiv p, reflection (a,b) & p9,b equiv p9, reflection (a,b) )
thus between p,b,p9 by A2; :: thesis: ( p,b equiv reflection (a,b),p & p,b equiv p, reflection (a,b) & p9,b equiv p9, reflection (a,b) )
reflection (a,p) = p9 by A1, DEFR;
then b,p9 equiv reflection (a,b), reflection (a,(reflection (a,p))) by Satz7p13;
then b,p9 equiv reflection (a,b),p by Satz7p7;
then b,p equiv reflection (a,b),p by A2, Satz2p3;
hence p,b equiv reflection (a,b),p by Satz2p4; :: thesis: ( p,b equiv p, reflection (a,b) & p9,b equiv p9, reflection (a,b) )
hence p,b equiv p, reflection (a,b) by Satz2p5; :: thesis: p9,b equiv p9, reflection (a,b)
b,p equiv reflection (a,b), reflection (a,p) by Satz7p13;
then b,p equiv reflection (a,b),p9 by A1, DEFR;
then b,p9 equiv reflection (a,b),p9 by A2, GTARSKI1:def 6;
then p9,b equiv reflection (a,b),p9 by Satz2p4;
hence p9,b equiv p9, reflection (a,b) by Satz2p5; :: thesis: verum
end;
then reflection (a,b) = b by Satz4p19;
hence a = b by Satz7p10; :: thesis: verum