let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct ; :: thesis: for a, p, p1, p2 being POINT of S st Middle p,a,p1 & Middle p,a,p2 holds
p1 = p2
let a be POINT of S; :: thesis: for p, p1, p2 being POINT of S st Middle p,a,p1 & Middle p,a,p2 holds
p1 = p2
let p, p1, p2 be POINT of S; :: thesis: ( Middle p,a,p1 & Middle p,a,p2 implies p1 = p2 )
assume A1: ( Middle p,a,p1 & Middle p,a,p2 ) ; :: thesis: p1 = p2
per cases ( p <> a or p = a ) ;
suppose A2: p <> a ; :: thesis: p1 = p2
( a,p1 equiv a,p & a,p2 equiv a,p ) by A1, Satz2p2;
hence p1 = p2 by A1, A2, Satz2p12; :: thesis: verum
end;
suppose p = a ; :: thesis: p1 = p2
then ( a = p1 & a = p2 ) by A1, Satz2p2, GTARSKI1:def 7;
hence p1 = p2 ; :: thesis: verum
end;
end;