let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct ; 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; 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; ( Middle p,a,p1 & Middle p,a,p2 implies p1 = p2 )
assume A1:
( Middle p,a,p1 & Middle p,a,p2 )
; p1 = p2