let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct ; :: thesis: for a, b, c, d, e, f being POINT of S st a,b equiv c,d & c,d equiv e,f holds
a,b equiv e,f
let a, b, c, d, e, f be POINT of S; :: thesis: ( a,b equiv c,d & c,d equiv e,f implies a,b equiv e,f )
assume A1: ( a,b equiv c,d & c,d equiv e,f ) ; :: thesis: a,b equiv e,f
then c,d equiv a,b by Satz2p2;
hence a,b equiv e,f by A1, GTARSKI1:def 6; :: thesis: verum