let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: 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 ) ; :: thesis: verum