let S be 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
let q, a, b, c be POINT of S; ( 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
; 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 verum
let x1,
x2 be
POINT of
S;
( 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 )
;
x1 = x2then
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;
verum
end;