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