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

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