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