for S being 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