let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b being POINT of S holds a,b equiv b,a
let a, b be POINT of S; :: thesis: a,b equiv b,a
S is satisfying_CongruenceSymmetry ;
hence a,b equiv b,a ; :: thesis: verum