let S be satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( a,b equiv c,d implies c,d equiv a,b )
assume A1: a,b equiv c,d ; :: thesis: c,d equiv a,b
a,b equiv a,b by Satz2p1bis;
hence c,d equiv a,b by A1, GTARSKI1:def 6; :: thesis: verum