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