let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c, q being POINT of S ex x being POINT of S st
( between q,a,x & a,x equiv b,c )
let a, b, c, q be POINT of S; ex x being POINT of S st
( between q,a,x & a,x equiv b,c )
S is satisfying_SegmentConstruction
;
hence
ex x being POINT of S st
( between q,a,x & a,x equiv b,c )
; verum