let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, q being POINT of S holds between q,a,a
let a, q be POINT of S; :: thesis: between q,a,a
consider x being POINT of S such that
X1: ( between q,a,x & a,x equiv a,a ) by A4;
thus between q,a,a by X1, A3; :: thesis: verum