let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, p, q, r, s being POINT of S st a,b equiv p,q & p,q equiv r,s holds
a,b equiv r,s
let a, b, p, q, r, s be POINT of S; :: thesis: ( a,b equiv p,q & p,q equiv r,s implies a,b equiv r,s )
assume that
X1: a,b equiv p,q and
X2: p,q equiv r,s ; :: thesis: a,b equiv r,s
p,q equiv a,b by X1, EquivSymmetric;
hence a,b equiv r,s by X2, A2; :: thesis: verum