:: deftheorem defines satisfying_SegmentConstruction GTARSKI1:def 8 :
for S being TarskiGeometryStruct holds
( S is satisfying_SegmentConstruction iff for a, q, b, c being POINT of S ex x being POINT of S st
( between q,a,x & a,x equiv b,c ) );