let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct ; for a, b, c, d being POINT of S st a,b equiv c,d holds
b,a equiv c,d
let a, b, c, d be POINT of S; ( a,b equiv c,d implies b,a equiv c,d )
assume A1:
a,b equiv c,d
; b,a equiv c,d
b,a equiv a,b
by GTARSKI1:def 5;
hence
b,a equiv c,d
by A1, Satz2p3; verum