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

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