let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st a,b equiv c,d holds
b,a equiv d,c
let a, b, c, d be POINT of S; :: thesis: ( a,b equiv c,d implies b,a equiv d,c )
X1: ( b,a equiv a,b & c,d equiv d,c ) by A1;
assume a,b equiv c,d ; :: thesis: b,a equiv d,c
then a,b equiv d,c by X1, EquivTransitive;
hence b,a equiv d,c by X1, EquivTransitive; :: thesis: verum