let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( a,b equiv c,d implies c,d equiv a,b )
assume H1:
a,b equiv c,d
; c,d equiv a,b
a,b equiv a,b
by EquivReflexive;
hence
c,d equiv a,b
by H1, A2; verum