theorem Satz2p12: :: GTARSKI3:12

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct
for q, a, b, c being POINT of S st q <> a holds
for x1, x2 being POINT of S st between q,a,x1 & a,x1 equiv b,c & between q,a,x2 & a,x2 equiv b,c holds
x1 = x2