let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct ; :: thesis: for a, b being POINT of S holds a,b equiv a,b
let a, b be POINT of S; :: thesis: a,b equiv a,b
b,a equiv a,b by GTARSKI1:def 5;
hence a,b equiv a,b by GTARSKI1:def 6; :: thesis: verum