let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st a,b equiv c,d holds

c,d equiv a,b

let a, b, c, d be POINT of S; :: thesis: ( a,b equiv c,d implies c,d equiv a,b )

assume H1: a,b equiv c,d ; :: thesis: c,d equiv a,b

a,b equiv a,b by EquivReflexive;

hence c,d equiv a,b by H1, A2; :: thesis: verum

c,d equiv a,b

let a, b, c, d be POINT of S; :: thesis: ( a,b equiv c,d implies c,d equiv a,b )

assume H1: a,b equiv c,d ; :: thesis: c,d equiv a,b

a,b equiv a,b by EquivReflexive;

hence c,d equiv a,b by H1, A2; :: thesis: verum