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