theorem Satz2p11:
for
S being
satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct for
a,
b,
c,
a9,
b9,
c9 being
POINT of
S st
between a,
b,
c &
between a9,
b9,
c9 &
a,
b equiv a9,
b9 &
b,
c equiv b9,
c9 holds
a,
c equiv a9,
c9