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