let S be satisfying_Tarski-model 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 A1;

hence a,b equiv a,b by A2; :: thesis: verum

let a, b be POINT of S; :: thesis: a,b equiv a,b

b,a equiv a,b by A1;

hence a,b equiv a,b by A2; :: thesis: verum