let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct ; :: thesis: for a, b, c, a9, b9, c9 being POINT of S st b,a,c cong b9,a9,c9 holds
a,b,c cong a9,b9,c9
let a, b, c, a9, b9, c9 be POINT of S; :: thesis: ( b,a,c cong b9,a9,c9 implies a,b,c cong a9,b9,c9 )
assume A1: b,a,c cong b9,a9,c9 ; :: thesis: a,b,c cong a9,b9,c9
then a,b equiv b9,a9 by Satz2p4;
hence a,b,c cong a9,b9,c9 by A1, Satz2p5; :: thesis: verum