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