let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct ; :: thesis: 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
let a, b, c, a9, b9, c9 be POINT of S; :: thesis: ( between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 implies a,c equiv a9,c9 )
assume A1: ( between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 ) ; :: thesis: a,c equiv a9,c9
A2: S is satisfying_SST_A5 ;
b,a equiv a9,b9 by A1, Satz2p4;
then A3: a,b,c,a AFS a9,b9,c9,a9 by A1, Satz2p5, Satz2p8;

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: a,c equiv a9,c9

hence a,c equiv a9,c9 by A1, Satz2p2, GTARSKI1:def 7; :: thesis: verum

end;

suppose a <> b ; :: thesis: a,c equiv a9,c9

then c,a equiv c9,a9 by A3, A2;
then a,c equiv c9,a9 by Satz2p4;
hence a,c equiv a9,c9 by Satz2p5; :: thesis: verum

end;

end;