let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( a,b equiv c,d implies a,b equiv d,c )
assume A1: a,b equiv c,d ; :: thesis: a,b equiv d,c
c,d equiv d,c by GTARSKI1:def 5;
hence a,b equiv d,c by A1, Satz2p3; :: thesis: verum