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

( 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