let S be satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct ; for a, b being POINT of S holds a,b equiv a,b
let a, b be POINT of S; a,b equiv a,b
ex c being POINT of S st
( between a,a,c & a,c equiv a,b )
by GTARSKI1:def 8;
hence
a,b equiv a,b
by GTARSKI1:def 6; verum