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