let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct ; :: thesis: 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
let q, a, b, c be POINT of S; :: thesis: ( q <> a implies 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 )
assume A1: q <> a ; :: thesis: 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
A2: S is satisfying_SST_A5 ;

hereby :: thesis: verum

let x1, x2 be POINT of S; :: thesis: ( between q,a,x1 & a,x1 equiv b,c & between q,a,x2 & a,x2 equiv b,c implies x1 = x2 )
assume A3: ( between q,a,x1 & a,x1 equiv b,c & between q,a,x2 & a,x2 equiv b,c ) ; :: thesis: x1 = x2
then b,c equiv a,x2 by Satz2p2;
then A4: a,x1 equiv a,x2 by A3, Satz2p3;
( q,a equiv q,a & a,x1 equiv a,x1 ) by Satz2p1;
then q,a,x1,x1 AFS q,a,x1,x2 by A3, A4, Satz2p11;
then x1,x1 equiv x1,x2 by A1, A2;
hence x1 = x2 by Satz2p2, GTARSKI1:def 7; :: thesis: verum

end;