let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct ; 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; ( a,c,b cong a9,c9,b9 implies a,b,c cong a9,b9,c9 )
assume A1:
a,c,b cong a9,c9,b9
; 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; verum